feat: Static EM

PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -110,7 +110,6 @@ structure HarmonicOscillator where
 
 namespace HarmonicOscillator
 
-
 variable (S : HarmonicOscillator)
 
 @[simp]

PhysLean/Electromagnetism/Dynamics/CurrentDensity.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.SpaceAndTime.SpaceTime.TimeSlice
+import PhysLean.SpaceAndTime.TimeAndSpace.ConstantTimeDist
 /-!
 
 # The Lorentz Current Density
@@ -41,6 +42,7 @@ The current density is given in terms of the charge density `ρ` and the current
 - D. The Lorentz current density as a distribution
   - D.1. The underlying charge density
   - D.2. The underlying current density
+- E. Of Static Charge density
 
 ## iv. References
 
@@ -279,5 +281,43 @@ noncomputable def currentDensity (c : SpeedOfLight) :
   map_smul' r J := by
     simp
 
+/-!
+
+## E. Of Static Charge density
+
+-/
+
+/-- The Lorentz current density associated with a static charge density. -/
+noncomputable def ofStaticChargeDensity {d : ℕ} (c : SpeedOfLight) :
+    ((Space d) →d[ℝ] ℝ) →ₗ[ℝ] DistLorentzCurrentDensity d where
+  toFun ρ :=
+    let smul : ℝ →L[ℝ] Lorentz.Vector d := {
+      toFun := fun r => r • Lorentz.Vector.basis (Sum.inl 0),
+      map_add' x y := by simp [add_smul],
+      map_smul' r x := by simp [smul_smul]
+    }
+    smul ∘L ((SpaceTime.distTimeSlice c).symm (c.1 • Space.constantTime  ρ))
+  map_add' ρ1 ρ2 := by
+    simp [map_add, ContinuousLinearMap.comp_add]
+  map_smul' r ρ := by
+    simp [map_smul, ContinuousLinearMap.comp_smulₛₗ, RingHom.id_apply,]
+    rw [smul_comm]
+
+@[simp]
+lemma ofStaticChargeDensity_currentDensity_eq_zero {d : ℕ} (c : SpeedOfLight)
+    (ρ : (Space d) →d[ℝ] ℝ) :
+    (ofStaticChargeDensity c ρ).currentDensity c = 0 := by
+  ext t i
+  simp [ofStaticChargeDensity, currentDensity, distTimeSlice, Space.constantTime]
+
+@[simp]
+lemma ofStaticChargeDensity_chargeDensity_eq {d : ℕ} (c : SpeedOfLight)
+    (ρ : (Space d) →d[ℝ] ℝ) :
+    (ofStaticChargeDensity c ρ).chargeDensity c = Space.constantTime ρ := by
+  ext f
+  simp [ofStaticChargeDensity, chargeDensity, Lorentz.Vector.temporalCLM, distTimeSlice_apply]
+  rw [← distTimeSlice_apply]
+  simp
+
 end DistLorentzCurrentDensity
 end Electromagnetism

PhysLean/Electromagnetism/Kinematics/EMPotential.lean

@@ -455,6 +455,34 @@ lemma deriv_equivariant {d} {A : DistElectromagneticPotential d}
     (Λ : LorentzGroup d) : deriv (Λ • A) = Λ • deriv A := by
   rw [deriv, distTensorDeriv_equivariant]
 
+/-!
+
+## D. Construction of the electromagnetic potential from a scalar and vector potential
+
+-/
+
+/-!
+
+## D.1. The electromagnetic potential of a scalar potential
+
+-/
+
+/-- The electromagnetic potential of a scalar potential. -/
+noncomputable def ofScalarPotential {d} (c : SpeedOfLight) :
+    ((Time × Space d) →d[ℝ] ℝ) →ₗ[ℝ] DistElectromagneticPotential d where
+  toFun ρ :=
+    let smul : ℝ →L[ℝ] Lorentz.Vector d := {
+      toFun := fun r => r • Lorentz.Vector.basis (Sum.inl 0),
+      map_add' x y := by simp [add_smul],
+      map_smul' r x := by simp [smul_smul]
+    }
+    smul ∘L ((SpaceTime.distTimeSlice c).symm (c.1⁻¹ • ρ))
+  map_add' ρ1 ρ2 := by
+    simp [map_add, ContinuousLinearMap.comp_add]
+  map_smul' r ρ := by
+    simp [map_smul, ContinuousLinearMap.comp_smulₛₗ]
+    rw [smul_comm]
+
 end DistElectromagneticPotential
 
 end Electromagnetism

PhysLean/Electromagnetism/Kinematics/ElectricField.lean

@@ -401,6 +401,11 @@ lemma electricField_eq_fieldStrength {d} {c : SpeedOfLight}
   field_simp
   ring
 
+lemma ofScalarPotential_electricField {d} (c : SpeedOfLight)
+    (V : (Time × Space d) →d[ℝ] ℝ) :
+    (ofScalarPotential c V).electricField c = - Space.distSpaceGrad V := by
+  simp [electricField]
+
 end DistElectromagneticPotential
 
 end Electromagnetism

PhysLean/Electromagnetism/Kinematics/MagneticField.lean

@@ -695,5 +695,19 @@ lemma magneticFieldMatrix_one_dim_eq_zero {c : SpeedOfLight}
   rw [magneticFieldMatrix_eq_vectorPotential]
   simp
 
+/-!
+
+### D.4. Magnetic field matrix of scalar potentials
+
+-/
+
+@[simp]
+lemma ofScalarPotential_magneticFieldMatrix {c : SpeedOfLight}
+    (V : (Time × Space d) →d[ℝ] ℝ)  :
+    (ofScalarPotential c V).magneticFieldMatrix c = 0 := by
+  ext ε
+  rw [magneticFieldMatrix_eq_vectorPotential]
+  simp
+
 end DistElectromagneticPotential
 end Electromagnetism

PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean

@@ -162,5 +162,14 @@ noncomputable def scalarPotential {d} (c : SpeedOfLight) :
       Function.comp_apply, Pi.smul_apply, smul_eq_mul, Real.ringHom_apply]
     ring
 
+@[simp]
+lemma ofScalarPotential_scalarPotential {d} (c : SpeedOfLight)
+    (V : (Time × Space d) →d[ℝ] ℝ) :
+    (ofScalarPotential c V).scalarPotential c = V := by
+  ext ε
+  simp [ofScalarPotential, scalarPotential, Lorentz.Vector.temporalCLM, distTimeSlice_apply]
+  rw [← distTimeSlice_apply]
+  simp
+
 end DistElectromagneticPotential
 end Electromagnetism

PhysLean/Electromagnetism/Kinematics/VectorPotential.lean

@@ -178,6 +178,13 @@ noncomputable def vectorPotential {d} (c : SpeedOfLight) :
       Pi.smul_apply, Function.comp_apply,
       Real.ringHom_apply, PiLp.smul_apply, smul_eq_mul]
 
+@[simp]
+lemma ofScalarPotential_vectorPotential {d} (c : SpeedOfLight)
+    (V : (Time × Space d) →d[ℝ] ℝ) :
+    (ofScalarPotential c V).vectorPotential c = 0 := by
+  ext ε
+  simp [ofScalarPotential, vectorPotential, Lorentz.Vector.spatialCLM, distTimeSlice_apply]
+
 end DistElectromagneticPotential
 
 end Electromagnetism

PhysLean/Electromagnetism/PointParticle/OneDimension.lean

@@ -53,38 +53,26 @@ namespace DistElectromagneticPotential
 /-- The current density of a point particle stationary at the origin
   of 1d space. -/
 noncomputable def oneDimPointParticleCurrentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) :
-    DistLorentzCurrentDensity 1 := (SpaceTime.distTimeSlice c).symm <|
-  constantTime ((c * q) • diracDelta' ℝ r₀ (Lorentz.Vector.basis (Sum.inl 0)))
+    DistLorentzCurrentDensity 1 := .ofStaticChargeDensity c (q • diracDelta ℝ r₀)
 
 lemma oneDimPointParticleCurrentDensity_eq_distTranslate (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) :
-    oneDimPointParticleCurrentDensity c q r₀ = ((SpaceTime.distTimeSlice c).symm <|
-    constantTime <|
-    distTranslate (basis.repr r₀) <|
-    ((c * q) • diracDelta' ℝ 0 (Lorentz.Vector.basis (Sum.inl 0)))) := by
+    oneDimPointParticleCurrentDensity c q r₀ =
+    .ofStaticChargeDensity c (q • distTranslate (basis.repr r₀) (diracDelta ℝ 0)) := by
   rw [oneDimPointParticleCurrentDensity]
   congr
   ext η
-  simp [distTranslate_apply]
+  simp
 
 @[simp]
 lemma oneDimPointParticleCurrentDensity_currentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) :
     (oneDimPointParticleCurrentDensity c q r₀).currentDensity c = 0 := by
-  ext ε i
-  simp [oneDimPointParticleCurrentDensity, DistLorentzCurrentDensity.currentDensity,
-    Lorentz.Vector.spatialCLM, constantTime_apply]
+  simp [oneDimPointParticleCurrentDensity]
 
 @[simp]
 lemma oneDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) :
     (oneDimPointParticleCurrentDensity c q r₀).chargeDensity c =
     constantTime (q • diracDelta ℝ r₀) := by
-  ext ε
-  simp only [DistLorentzCurrentDensity.chargeDensity, one_div, Lorentz.Vector.temporalCLM,
-    Fin.isValue, oneDimPointParticleCurrentDensity, map_smul, LinearMap.coe_mk, AddHom.coe_mk,
-    ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.coe_smul',
-    ContinuousLinearMap.coe_comp', LinearMap.coe_toContinuousLinearMap', Pi.smul_apply,
-    Function.comp_apply, constantTime_apply, diracDelta'_apply, Lorentz.Vector.apply_smul,
-    Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul, diracDelta_apply]
-  field_simp
+  simp [oneDimPointParticleCurrentDensity]
 
 /-!
 
@@ -101,16 +89,14 @@ lemma oneDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : 
 /-- The electromagnetic potential of a point particle stationary at `r₀`
   of 1d space. -/
 noncomputable def oneDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
-    DistElectromagneticPotential 1 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <|
-  distOfFunction (fun x => ((- (q * 𝓕.μ₀ * 𝓕.c)/ 2) * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0))
-    (by fun_prop)
+    DistElectromagneticPotential 1 := .ofScalarPotential 𝓕.c <| constantTime <|
+  ⸨x => ((- (q * 𝓕.μ₀ * 𝓕.c ^ 2)/ 2) * ‖x - r₀‖)⸩ᵈ
 
 lemma oneDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
-    oneDimPointParticle 𝓕 q r₀ = ((SpaceTime.distTimeSlice 𝓕.c).symm <|
+    oneDimPointParticle 𝓕 q r₀ = (.ofScalarPotential 𝓕.c <|
     constantTime <|
     distTranslate (basis.repr r₀) <|
-    distOfFunction (fun x => ((- (q * 𝓕.μ₀ * 𝓕.c)/ 2) * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0))
-      (by fun_prop)) := by
+    ⸨x => ((- (q * 𝓕.μ₀ * 𝓕.c ^ 2)/ 2) * ‖x‖)⸩ᵈ) := by
   rw [oneDimPointParticle]
   congr
   ext η
@@ -125,9 +111,7 @@ lemma oneDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ :
 @[simp]
 lemma oneDimPointParticle_vectorPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
     (oneDimPointParticle 𝓕 q r₀).vectorPotential 𝓕.c = 0 := by
-  ext ε i
-  simp [vectorPotential, Lorentz.Vector.spatialCLM,
-    oneDimPointParticle, constantTime_apply, distOfFunction_vector_eval]
+  simp [oneDimPointParticle]
 
 /-!
 
@@ -137,20 +121,9 @@ lemma oneDimPointParticle_vectorPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : S
 
 lemma oneDimPointParticle_scalarPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
     (oneDimPointParticle 𝓕 q r₀).scalarPotential 𝓕.c =
-    Space.constantTime (distOfFunction (fun x =>
-      - ((q * 𝓕.μ₀ * 𝓕.c ^ 2)/(2)) • ‖x-r₀‖) (by fun_prop)) := by
-  ext ε
-  simp only [scalarPotential, Lorentz.Vector.temporalCLM, Fin.isValue, map_smul,
-    ContinuousLinearMap.comp_smulₛₗ, Real.ringHom_apply, oneDimPointParticle, LinearMap.coe_mk,
-    AddHom.coe_mk, ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.coe_smul',
-    ContinuousLinearMap.coe_comp', LinearMap.coe_toContinuousLinearMap', Pi.smul_apply,
-    Function.comp_apply, constantTime_apply, distOfFunction_vector_eval, Lorentz.Vector.apply_smul,
-    Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul, neg_mul]
-  rw [distOfFunction_mul_fun _ (by fun_prop), distOfFunction_neg,
-    distOfFunction_mul_fun _ (by fun_prop)]
-  simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul,
-    ContinuousLinearMap.neg_apply]
-  ring
+    Space.constantTime ⸨x => - ((q * 𝓕.μ₀ * 𝓕.c ^ 2)/2) • ‖x-r₀‖⸩ᵈ := by
+  simp [oneDimPointParticle]
+  ring_nf
 
 /-!
 

PhysLean/Electromagnetism/PointParticle/ThreeDimension.lean

@@ -62,19 +62,16 @@ particle in 3d space.
 /-- The current density of a point particle stationary at a point `r₀`
   of 3d space. -/
 noncomputable def threeDimPointParticleCurrentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 3) :
-    DistLorentzCurrentDensity 3 := (SpaceTime.distTimeSlice c).symm <|
-  constantTime ((c * q) • diracDelta' ℝ r₀ (Lorentz.Vector.basis (Sum.inl 0)))
+    DistLorentzCurrentDensity 3 := .ofStaticChargeDensity c (q • diracDelta ℝ r₀)
 
 lemma threeDimPointParticleCurrentDensity_eq_distTranslate (c : SpeedOfLight) (q : ℝ)
     (r₀ : Space 3) :
-    threeDimPointParticleCurrentDensity c q r₀ = ((SpaceTime.distTimeSlice c).symm <|
-    constantTime <|
-    distTranslate (basis.repr r₀) <|
-    ((c * q) • diracDelta' ℝ 0 (Lorentz.Vector.basis (Sum.inl 0)))) := by
+    threeDimPointParticleCurrentDensity c q r₀ =
+    .ofStaticChargeDensity c (q • distTranslate (basis.repr r₀) (diracDelta ℝ 0)) := by
   rw [threeDimPointParticleCurrentDensity]
   congr
   ext η
-  simp [distTranslate_apply]
+  simp
 
 /-!
 
@@ -91,14 +88,7 @@ where $q$ is the charge of the particle and $r₀$ is the position of the partic
 lemma threeDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 3) :
     (threeDimPointParticleCurrentDensity c q r₀).chargeDensity c =
     constantTime (q • diracDelta ℝ r₀) := by
-  ext ε
-  simp only [DistLorentzCurrentDensity.chargeDensity, one_div, Lorentz.Vector.temporalCLM,
-    Fin.isValue, threeDimPointParticleCurrentDensity, map_smul, LinearMap.coe_mk, AddHom.coe_mk,
-    ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.coe_smul',
-    ContinuousLinearMap.coe_comp', LinearMap.coe_toContinuousLinearMap', Pi.smul_apply,
-    Function.comp_apply, constantTime_apply, diracDelta'_apply, Lorentz.Vector.apply_smul,
-    Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul, diracDelta_apply]
-  field_simp
+  simp [threeDimPointParticleCurrentDensity]
 
 /-!
 
@@ -114,9 +104,7 @@ In other words, there is no current flow for a point particle at rest.
 @[simp]
 lemma threeDimPointParticleCurrentDensity_currentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 3) :
     (threeDimPointParticleCurrentDensity c q r₀).currentDensity c = 0 := by
-  ext ε i
-  simp [threeDimPointParticleCurrentDensity, DistLorentzCurrentDensity.currentDensity,
-    Lorentz.Vector.spatialCLM, constantTime_apply]
+  simp [threeDimPointParticleCurrentDensity]
 
 /-!
 
@@ -141,18 +129,15 @@ open Real
 /-- The electromagnetic potential of a point particle stationary at `r₀`
   of 3d space. -/
 noncomputable def threeDimPointParticle (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) :
-    DistElectromagneticPotential 3 := (SpaceTime.distTimeSlice 𝓕.c).symm <| Space.constantTime <|
-  distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c)/ (4 * π)) * ‖x - r₀‖⁻¹) •
-    Lorentz.Vector.basis (Sum.inl 0))
-    (((IsDistBounded.inv_shift _).const_mul_fun _).smul_const _)
+    DistElectromagneticPotential 3 := .ofScalarPotential 𝓕.c <| Space.constantTime <|
+  ⸨x => ((q * 𝓕.μ₀ * 𝓕.c ^ 2)/ (4 * π)) * ‖x - r₀‖⁻¹⸩ᵈ
 
 lemma threeDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) :
-    threeDimPointParticle 𝓕 q r₀ = ((SpaceTime.distTimeSlice 𝓕.c).symm <|
+    threeDimPointParticle 𝓕 q r₀ = (.ofScalarPotential 𝓕.c <|
     constantTime <|
     distTranslate (basis.repr r₀) <|
-    distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c)/ (4 * π))* ‖x‖⁻¹) •
-      Lorentz.Vector.basis (Sum.inl 0))
-      ((IsDistBounded.inv.const_mul_fun _).smul_const _)) := by
+    distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c ^ 2)/ (4 * π))* ‖x‖⁻¹))
+      (IsDistBounded.inv.const_mul_fun _)) := by
   rw [threeDimPointParticle]
   congr
   ext η
@@ -171,22 +156,10 @@ $$V(r) = \frac{q}{4 π \epsilon_0 |r - r_0|}.$$
 
 lemma threeDimPointParticle_scalarPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) :
     (threeDimPointParticle 𝓕 q r₀).scalarPotential 𝓕.c =
-    Space.constantTime (distOfFunction (fun x => (q/ (4 * π * 𝓕.ε₀))• ‖x - r₀‖⁻¹)
-      (((IsDistBounded.inv_shift _).const_mul_fun _))) := by
-  ext ε
-  simp only [scalarPotential, Lorentz.Vector.temporalCLM, Fin.isValue, map_smul,
-    ContinuousLinearMap.comp_smulₛₗ, ringHom_apply, threeDimPointParticle, LinearMap.coe_mk,
-    AddHom.coe_mk, ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.coe_smul',
-    ContinuousLinearMap.coe_comp', LinearMap.coe_toContinuousLinearMap', Pi.smul_apply,
-    Function.comp_apply, constantTime_apply, distOfFunction_vector_eval, Lorentz.Vector.apply_smul,
-    Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul]
-  rw [distOfFunction_mul_fun _ (IsDistBounded.inv_shift _),
-    distOfFunction_mul_fun _ (IsDistBounded.inv_shift _)]
-  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, ContinuousLinearMap.coe_smul', Pi.smul_apply,
-    smul_eq_mul]
-  ring_nf
-  simp only [𝓕.c_sq, one_div, mul_inv_rev, mul_eq_mul_right_iff, inv_eq_zero, OfNat.ofNat_ne_zero,
-    or_false]
+    Space.constantTime ⸨x => (q/ (4 * π * 𝓕.ε₀))• ‖x - r₀‖⁻¹⸩ᵈ := by
+  simp [threeDimPointParticle, 𝓕.c_sq]
+  congr
+  funext x
   field_simp
 
 /-!
@@ -203,9 +176,7 @@ $$\vec A(r) = 0.$$
 @[simp]
 lemma threeDimPointParticle_vectorPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 3) :
     (threeDimPointParticle 𝓕 q r₀).vectorPotential 𝓕.c = 0 := by
-  ext ε i
-  simp [vectorPotential, Lorentz.Vector.spatialCLM,
-    threeDimPointParticle, constantTime_apply, distOfFunction_vector_eval]
+  simp [threeDimPointParticle]
 
 /-!
 
@@ -255,9 +226,7 @@ Given that the vector potential is zero, the magnetic field is also zero.
 
 @[simp]
 lemma threeDimPointParticle_magneticFieldMatrix (q : ℝ) (r₀ : Space 3) :
-    (threeDimPointParticle 𝓕 q r₀).magneticFieldMatrix 𝓕.c = 0 := by
-  ext η
-  simp [magneticFieldMatrix_eq_vectorPotential]
+    (threeDimPointParticle 𝓕 q r₀).magneticFieldMatrix 𝓕.c = 0 := by simp [threeDimPointParticle]
 
 /-!