Skip to content

Commit f2cc276

Browse files
jstoobysmithjstoobysmith
authored
refactor: Move distributional EM to new file system (#1118)
* move: DistElectromagneticPotential * rm: DistElectromagneticPotential * move: scalarPotential * rm: scalarPotential * move: vectorPotential * rm: vectorPotential * move: FieldStrength * rm: FieldStrength * move: ElectricField * rm: ElectricField * move: MagneticFields * rm: MagneticFields * move: KineticTerm * rm: KineticTerm * move: CurrentDensity * rm: CurrentDensity * move: Lagrangian * rm: Lagrangian * move: IsExtrema * rm: IsExtrema * fix: Examples * fix: imports * docs: rm old docs * docs: fix new docs
1 parent 9674ea4 commit f2cc276

24 files changed

Lines changed: 1737 additions & 1298 deletions

‎Physlib.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,16 @@ public import Physlib.Electromagnetism.Basic
3030
public import Physlib.Electromagnetism.Charge.ChargeUnit
3131
public import Physlib.Electromagnetism.Current.CircularCoil
3232
public import Physlib.Electromagnetism.Current.InfiniteWire
33+
public import Physlib.Electromagnetism.Distributional.Basic
34+
public import Physlib.Electromagnetism.Distributional.Dynamics.CurrentDensity
35+
public import Physlib.Electromagnetism.Distributional.Dynamics.IsExtrema
36+
public import Physlib.Electromagnetism.Distributional.Dynamics.KineticTerm
37+
public import Physlib.Electromagnetism.Distributional.Dynamics.Lagrangian
38+
public import Physlib.Electromagnetism.Distributional.ElectricField
39+
public import Physlib.Electromagnetism.Distributional.FieldStrength
40+
public import Physlib.Electromagnetism.Distributional.MagneticField
41+
public import Physlib.Electromagnetism.Distributional.ScalarPotential
42+
public import Physlib.Electromagnetism.Distributional.VectorPotential
3343
public import Physlib.Electromagnetism.Dynamics.Basic
3444
public import Physlib.Electromagnetism.Dynamics.CurrentDensity
3545
public import Physlib.Electromagnetism.Dynamics.Hamiltonian

‎Physlib/Electromagnetism/Current/InfiniteWire.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
55
-/
66
module
77

8-
public import Physlib.Electromagnetism.Dynamics.IsExtrema
8+
public import Physlib.Electromagnetism.Distributional.Dynamics.IsExtrema
99
public import Physlib.SpaceAndTime.Space.Norm
1010
public import Physlib.SpaceAndTime.Space.ConstantSliceDist
1111
public import Physlib.SpaceAndTime.TimeAndSpace.ConstantTimeDist

‎Physlib/Electromagnetism/Distributional/Basic.lean‎

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
/-
2+
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joseph Tooby-Smith
5+
-/
6+
module
7+
8+
public import Physlib.SpaceAndTime.SpaceTime.Derivatives
9+
public import Physlib.SpaceAndTime.Space.Derivatives.Curl
10+
public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
11+
public import Physlib.Relativity.Tensors.Elab
12+
public import Physlib.SpaceAndTime.SpaceTime.TimeSlice
13+
14+
/-!
15+
16+
# The Electromagnetic Potential
17+
18+
## i. Overview
19+
20+
The electromagnetic potential `A^μ` is the fundamental objects in
21+
electromagnetism. Mathematically it is related to a connection
22+
on a `U(1)`-bundle.
23+
24+
We define the electromagnetic potential as a distribution from
25+
spacetime to contravariant Lorentz vectors.
26+
27+
## ii. Key results
28+
29+
- `DistElectromagneticPotential` : the type of electromagnetic potentials as distributions.
30+
31+
## iii. Table of contents
32+
33+
- A. The electromagnetic potential as a distribution
34+
- A.1. The derivative of the electromagnetic potential as a distribution
35+
- A.2. The derivative in terms of the basis
36+
- A.3. Equivariance of the derivative distribution
37+
38+
## iv. References
39+
40+
- https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
41+
- https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf
42+
43+
-/
44+
45+
@[expose] public section
46+
47+
namespace Electromagnetism
48+
open Module realLorentzTensor
49+
open IndexNotation
50+
open TensorSpecies
51+
open Tensor
52+
53+
/-!
54+
55+
## A. The electromagnetic potential as a distribution
56+
57+
-/
58+
59+
/-- The electromagnetic potential as a distribution and as a tensor `A^μ`. -/
60+
noncomputable abbrev DistElectromagneticPotential (d : ℕ := 3) :=
61+
(SpaceTime d) →d[ℝ] Lorentz.Vector d
62+
63+
namespace DistElectromagneticPotential
64+
open TensorSpecies
65+
open Tensor
66+
open SpaceTime
67+
open TensorProduct
68+
open minkowskiMatrix SchwartzMap
69+
attribute [-simp] Fintype.sum_sum_type
70+
attribute [-simp] Nat.succ_eq_add_one
71+
72+
/-!
73+
74+
### A.1. The derivative of the electromagnetic potential as a distribution
75+
76+
-/
77+
78+
set_option backward.isDefEq.respectTransparency false in
79+
/-- The derivative of a electromagnetic potential, which is a distribution. -/
80+
noncomputable def deriv {d} : DistElectromagneticPotential d →ₗ[ℝ]
81+
(SpaceTime d) →d[ℝ] Lorentz.CoVector d ⊗[ℝ] Lorentz.Vector d := distTensorDeriv
82+
83+
set_option backward.isDefEq.respectTransparency false in
84+
lemma deriv_eq_sum_sum {d} (A : DistElectromagneticPotential d)
85+
(ε : 𝓢(SpaceTime d, ℝ)) :
86+
deriv A ε =∑ μ, ∑ ν, (SpaceTime.distDeriv μ A ε ν) •
87+
Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν := by
88+
simp [deriv, distTensorDeriv_apply]
89+
congr
90+
funext μ
91+
conv_lhs => rw [← Lorentz.Vector.basis.sum_repr (SpaceTime.distDeriv μ A ε)]
92+
rw [tmul_sum]
93+
congr
94+
funext ν
95+
simp
96+
rfl
97+
/-!
98+
99+
### A.2. The derivative in terms of the basis
100+
101+
-/
102+
103+
@[simp]
104+
lemma deriv_basis_repr_apply {d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)}
105+
(A : DistElectromagneticPotential d)
106+
(ε : 𝓢(SpaceTime d, ℝ)) :
107+
(Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (deriv A ε) μν =
108+
distDeriv μν.1 A ε μν.2 := by
109+
match μν with
110+
| (μ, ν) =>
111+
rw [deriv_eq_sum_sum]
112+
simp only [map_sum, map_smul, Finsupp.coe_finset_sum, Finsupp.coe_smul, Finset.sum_apply,
113+
Pi.smul_apply, Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, smul_eq_mul]
114+
rw [Finset.sum_eq_single μ, Finset.sum_eq_single ν]
115+
· simp
116+
· intro μ' _ h
117+
simp [h]
118+
· simp
119+
· intro ν' _ h
120+
simp [h]
121+
· simp
122+
123+
lemma toTensor_deriv_basis_repr_apply {d} (A : DistElectromagneticPotential d)
124+
(ε : 𝓢(SpaceTime d, ℝ)) (b : ComponentIdx (S := realLorentzTensor d)
125+
(Fin.append ![Color.down] ![Color.up])) :
126+
(Tensor.basis _).repr (Tensorial.toTensor (deriv A ε)) b =
127+
distDeriv (b 0) A ε (b 1) := by
128+
rw [Tensorial.basis_toTensor_apply]
129+
rw [Tensorial.basis_map_prod]
130+
simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
131+
Equiv.symm_symm, Fin.isValue]
132+
rw [Lorentz.Vector.tensor_basis_map_eq_basis_reindex,
133+
Lorentz.CoVector.tensor_basis_map_eq_basis_reindex]
134+
have hb : (((Lorentz.CoVector.basis (d := d)).reindex
135+
Lorentz.CoVector.indexEquiv.symm).tensorProduct
136+
(Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)) =
137+
((Lorentz.CoVector.basis (d := d)).tensorProduct (Lorentz.Vector.basis (d := d))).reindex
138+
(Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm) := by
139+
ext b
140+
match b with
141+
| ⟨i, j⟩ =>
142+
simp
143+
rw [hb]
144+
rw [Module.Basis.repr_reindex_apply, deriv_basis_repr_apply]
145+
rfl
146+
147+
/-!
148+
149+
### A.3. Equivariance of the derivative distribution
150+
151+
-/
152+
153+
set_option backward.isDefEq.respectTransparency false in
154+
lemma deriv_equivariant {d} {A : DistElectromagneticPotential d}
155+
(Λ : LorentzGroup d) : deriv (Λ • A) = Λ • deriv A := by
156+
rw [deriv, distTensorDeriv_equivariant]
157+
158+
end DistElectromagneticPotential
159+
160+
end Electromagnetism

‎Physlib/Electromagnetism/Distributional/Dynamics/CurrentDensity.lean‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
/-
2+
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joseph Tooby-Smith
5+
-/
6+
module
7+
8+
public import Physlib.SpaceAndTime.SpaceTime.TimeSlice
9+
/-!
10+
11+
# The Lorentz Current Density
12+
13+
## i. Overview
14+
15+
In this module we define the Lorentz current density
16+
and its decomposition into charge density and current density.
17+
The Lorentz current density is often called the four-current and given then the symbol `J`.
18+
19+
The current density is given in terms of the charge density `ρ` and the current density
20+
` \vec j` as `J = (c ρ, \vec j)`.
21+
22+
## ii. Key results
23+
24+
- `DistLorentzCurrentDensity` : The type of Lorentz current densities
25+
as distributions.
26+
27+
## iii. Table of contents
28+
29+
- A. The Lorentz current density as a distribution
30+
- A.1. The underlying charge density
31+
- A.2. The underlying current density
32+
33+
## iv. References
34+
35+
-/
36+
37+
@[expose] public section
38+
39+
namespace Electromagnetism
40+
open TensorSpecies
41+
open SpaceTime
42+
open TensorProduct
43+
open minkowskiMatrix
44+
open InnerProductSpace
45+
46+
attribute [-simp] Fintype.sum_sum_type
47+
attribute [-simp] Nat.succ_eq_add_one
48+
49+
/-!
50+
51+
## A. The Lorentz current density as a distribution
52+
53+
-/
54+
/-- The Lorentz current density, also called four-current as a distribution. -/
55+
abbrev DistLorentzCurrentDensity (d : ℕ := 3) := (SpaceTime d) →d[ℝ] Lorentz.Vector d
56+
57+
namespace DistLorentzCurrentDensity
58+
59+
/-!
60+
61+
### A.1. The underlying charge density
62+
63+
-/
64+
65+
set_option backward.isDefEq.respectTransparency false in
66+
/-- The charge density underlying a Lorentz current density which is a distribution. -/
67+
noncomputable def chargeDensity {d : ℕ} (c : SpeedOfLight) :
68+
(DistLorentzCurrentDensity d) →ₗ[ℝ] (Time × Space d) →d[ℝ] ℝ where
69+
toFun J := (1 / (c : ℝ)) • (Lorentz.Vector.temporalCLM d ∘L distTimeSlice c J)
70+
map_add' J1 J2 := by
71+
simp
72+
map_smul' r J := by
73+
simp only [one_div, map_smul, ContinuousLinearMap.comp_smulₛₗ, RingHom.id_apply]
74+
rw [smul_comm]
75+
76+
/-!
77+
78+
### A.2. The underlying current density
79+
80+
-/
81+
82+
set_option backward.isDefEq.respectTransparency false in
83+
/-- The underlying (non-Lorentz) current density associated with a distributive
84+
Lorentz current density. -/
85+
noncomputable def currentDensity (c : SpeedOfLight) :
86+
DistLorentzCurrentDensity d →ₗ[ℝ] (Time × Space d) →d[ℝ] EuclideanSpace ℝ (Fin d) where
87+
toFun J := Lorentz.Vector.spatialCLM d ∘L distTimeSlice c J
88+
map_add' J1 J2 := by
89+
simp
90+
map_smul' r J := by
91+
simp
92+
93+
end DistLorentzCurrentDensity
94+
end Electromagnetism

0 commit comments

Comments
 (0)