Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Electromagnetism.Distributional.Dynamics.IsExtrema
public import Physlib.SpaceAndTime.Space.Norm.Basic
public import Physlib.SpaceAndTime.Space.TranslationsElectrostatics of a stationary point particle in 3d
i. Overview
In this module we give the electromagnetic properties of a point particle sitting at the origin in 3d space.
ii. Key results
threeDimPointParticle : The electromagnetic potential of a point particle
stationary at a point in 3d space.
threeDimPointParticle_isExterma : The electric field of a point
particle stationary at a point of 3d space satisfies Maxwell's equations
iii. Table of contents
A. The current density
A.1. The charge density
A.2. The 3-current density
B. The Potentials
B.1. The electromagnetic potential
B.2. The scalar potential
B.3. The vector potential is zero
C. The electric field
C.1. the time derivative of the electric field
D. The magnetic field
E. Maxwell's equations
iv. References
@[expose] public sectionA. The current density
The current density of a point particle in 3d space is given by:
$$J(r) = (c q \delta(r - rโ), 0, 0, 0) $$
where $c$ is the speed light, $q$ is the charge of the particle and $rโ$ is the position of the particle in 3d space.
c:SpeedOfLightq:โrโ:Spaceโข (SpaceTime.distTimeSlice c).symm (constantTime ((c.val * q) โข diracDelta' โ rโ (Lorentz.Vector.basis (Sum.inl 0)))) =
(SpaceTime.distTimeSlice c).symm
(constantTime ((distTranslate (basis.repr rโ)) ((c.val * q) โข diracDelta' โ 0 (Lorentz.Vector.basis (Sum.inl 0)))))
congr e_6.e_6 c:SpeedOfLightq:โrโ:Spaceโข (c.val * q) โข diracDelta' โ rโ (Lorentz.Vector.basis (Sum.inl 0)) =
(distTranslate (basis.repr rโ)) ((c.val * q) โข diracDelta' โ 0 (Lorentz.Vector.basis (Sum.inl 0)))
ext ฮท e_6.e_6 c:SpeedOfLightq:โrโ:Spaceฮท:๐ข(Space, โ)iโ:Fin 1 โ Fin 3โข ((c.val * q) โข diracDelta' โ rโ (Lorentz.Vector.basis (Sum.inl 0))) ฮท iโ =
((distTranslate (basis.repr rโ)) ((c.val * q) โข diracDelta' โ 0 (Lorentz.Vector.basis (Sum.inl 0)))) ฮท iโ
simp [distTranslate_apply] All goals completed! ๐A.1. The charge density
The charge density of a point particle in 3d space is given by: $$ฯ(r) = q \delta(r - rโ) $$
where $q$ is the charge of the particle and $rโ$ is the position of the particle in 3d space.
@[simp]
lemma threeDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : โ) (rโ : Space 3) :
(threeDimPointParticleCurrentDensity c q rโ).chargeDensity c =
constantTime (q โข diracDelta โ rโ) := by c:SpeedOfLightq:โrโ:Spaceโข (DistLorentzCurrentDensity.chargeDensity c) (threeDimPointParticleCurrentDensity c q rโ) =
constantTime (q โข diracDelta โ rโ)
ext ฮต c:SpeedOfLightq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ((DistLorentzCurrentDensity.chargeDensity c) (threeDimPointParticleCurrentDensity c q rโ)) ฮต =
(constantTime (q โข diracDelta โ rโ)) ฮต
simp only [DistLorentzCurrentDensity.chargeDensity, one_div, Lorentz.Vector.temporalCLM,
Fin.isValue, threeDimPointParticleCurrentDensity, map_smul, LinearMap.coe_mk, AddHom.coe_mk,
ContinuousLinearEquiv.apply_symm_apply, FunLike.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] c:SpeedOfLightq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข c.val * q * (c.valโปยน * (timeIntegralSchwartz ฮต) rโ) = q * (timeIntegralSchwartz ฮต) rโ
field_simp All goals completed! ๐A.2. The 3-current density
The 3-current density of a point particle in 3d space is given by: $$\vec J(r) = 0.$$
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 c:SpeedOfLightq:โrโ:Spaceโข (DistLorentzCurrentDensity.currentDensity c) (threeDimPointParticleCurrentDensity c q rโ) = 0
ext ฮต i c:SpeedOfLightq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)i:Fin 3โข (((DistLorentzCurrentDensity.currentDensity c) (threeDimPointParticleCurrentDensity c q rโ)) ฮต).ofLp i = (0 ฮต).ofLp i
simp [threeDimPointParticleCurrentDensity, DistLorentzCurrentDensity.currentDensity,
Lorentz.Vector.spatialCLM, constantTime_apply] All goals completed! ๐B. The Potentials
B.1. The electromagnetic potential
The 4-potential of a point particle in 3d space is given by:
$$A(r) = \frac{q ฮผโ c}{4 ฯ |r - rโ|} (1, 0, 0, 0) $$
where $ฮผโ$ is the permeability of free space, $c$ is the speed of light, $q$ is the charge of the particle and $rโ$ is the position of the particle in 3d space.
lemma threeDimPointParticle_eq_distTranslate (๐ : FreeSpace) (q : โ) (rโ : Space 3) :
threeDimPointParticle ๐ q rโ = ((SpaceTime.distTimeSlice ๐.c).symm <|
constantTime <|
distTranslate (basis.repr rโ) <|
distOfFunction (fun x => (((q * ๐.ฮผโ * ๐.c)/ (4 * ฯ))* โxโโปยน) โข
Lorentz.Vector.basis (Sum.inl 0))
(((IsDistBounded.inv (by ๐:FreeSpaceq:โrโ:Spaceโข 2 โค 3 norm_num All goals completed! ๐)).const_mul_fun _).smul_const _)) := by ๐:FreeSpaceq:โrโ:Spaceโข threeDimPointParticle ๐ q rโ =
(SpaceTime.distTimeSlice ๐.c).symm
(constantTime
((distTranslate (basis.repr rโ))
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โxโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ)))
rw [threeDimPointParticle ๐:FreeSpaceq:โrโ:Spaceโข (SpaceTime.distTimeSlice ๐.c).symm
(constantTime
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โx - rโโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ)) =
(SpaceTime.distTimeSlice ๐.c).symm
(constantTime
((distTranslate (basis.repr rโ))
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โxโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ))) ๐:FreeSpaceq:โrโ:Spaceโข (SpaceTime.distTimeSlice ๐.c).symm
(constantTime
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โx - rโโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ)) =
(SpaceTime.distTimeSlice ๐.c).symm
(constantTime
((distTranslate (basis.repr rโ))
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โxโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ)))] ๐:FreeSpaceq:โrโ:Spaceโข (SpaceTime.distTimeSlice ๐.c).symm
(constantTime
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โx - rโโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ)) =
(SpaceTime.distTimeSlice ๐.c).symm
(constantTime
((distTranslate (basis.repr rโ))
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โxโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ)))
congr e_6.e_6 ๐:FreeSpaceq:โrโ:Spaceโข distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โx - rโโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ =
(distTranslate (basis.repr rโ))
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โxโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ)
ext ฮท e_6.e_6 ๐:FreeSpaceq:โrโ:Spaceฮท:๐ข(Space, โ)iโ:Fin 1 โ Fin 3โข (distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โx - rโโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ) ฮท iโ =
((distTranslate (basis.repr rโ))
(distOfFunction (fun x => (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โxโโปยน) โข Lorentz.Vector.basis (Sum.inl 0)) โฏ))
ฮท iโ
simp [distTranslate_ofFunction] All goals completed! ๐B.2. The scalar potential
The first component of the 4-potential is the scalar potential, once one has taken account of factors of the speed of light. It is given by:
$$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 ๐:FreeSpaceq:โrโ:Spaceโข (scalarPotential ๐.c) (threeDimPointParticle ๐ q rโ) =
constantTime (distOfFunction (fun x => (q / (4 * ฯ * ๐.ฮตโ)) โข โx - rโโโปยน) โฏ)
ext ฮต ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ((scalarPotential ๐.c) (threeDimPointParticle ๐ q rโ)) ฮต =
(constantTime (distOfFunction (fun x => (q / (4 * ฯ * ๐.ฮตโ)) โข โx - rโโโปยน) โฏ)) ฮต
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, FunLike.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] ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.c.val * (distOfFunction (fun x => q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) =
(distOfFunction (fun x => q / (4 * ฯ * ๐.ฮตโ) * โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต)
rw [distOfFunction_mul_fun _ (IsDistBounded.inv_shift _), ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.c.val * ((q * ๐.ฮผโ * ๐.c.val / (4 * ฯ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) =
(distOfFunction (fun x => q / (4 * ฯ * ๐.ฮตโ) * โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.c.val * ((q * ๐.ฮผโ * ๐.c.val / (4 * ฯ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) =
((q / (4 * ฯ * ๐.ฮตโ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต)
distOfFunction_mul_fun _ (IsDistBounded.inv_shift _) ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.c.val * ((q * ๐.ฮผโ * ๐.c.val / (4 * ฯ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) =
((q / (4 * ฯ * ๐.ฮตโ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.c.val * ((q * ๐.ฮผโ * ๐.c.val / (4 * ฯ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) =
((q / (4 * ฯ * ๐.ฮตโ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต)] ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.c.val * ((q * ๐.ฮผโ * ๐.c.val / (4 * ฯ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) =
((q / (4 * ฯ * ๐.ฮตโ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต)
simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul] ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.c.val * (q * ๐.ฮผโ * ๐.c.val / (4 * ฯ) * (distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต)) =
q / (4 * ฯ * ๐.ฮตโ) * (distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต)
ring_nf ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.c.val ^ 2 * q * ๐.ฮผโ * ฯโปยน * (distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) * (1 / 4) =
q * ฯโปยน * (distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) * ๐.ฮตโโปยน * (1 / 4)
simp only [๐.c_sq, one_div, mul_inv_rev, mul_eq_mul_right_iff, inv_eq_zero, OfNat.ofNat_ne_zero,
or_false] ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)โข ๐.ฮผโโปยน * ๐.ฮตโโปยน * q * ๐.ฮผโ * ฯโปยน * (distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) =
q * ฯโปยน * (distOfFunction (fun x => โx - rโโโปยน) โฏ) (timeIntegralSchwartz ฮต) * ๐.ฮตโโปยน
field_simp All goals completed! ๐B.3. The vector potential is zero
The spatial components of the 4-potential give the vector potential, which is zero for a stationary point particle.
$$\vec A(r) = 0.$$
@[simp]
lemma threeDimPointParticle_vectorPotential (๐ : FreeSpace) (q : โ) (rโ : Space 3) :
(threeDimPointParticle ๐ q rโ).vectorPotential ๐.c = 0 := by ๐:FreeSpaceq:โrโ:Spaceโข (vectorPotential ๐.c) (threeDimPointParticle ๐ q rโ) = 0
ext ฮต i ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(Time ร Space, โ)i:Fin 3โข (((vectorPotential ๐.c) (threeDimPointParticle ๐ q rโ)) ฮต).ofLp i = (0 ฮต).ofLp i
simp [vectorPotential, Lorentz.Vector.spatialCLM,
threeDimPointParticle, constantTime_apply, distOfFunction_vector_eval] All goals completed! ๐C. The electric field
The electric field of a point particle in 3d space is given by: $$\vec E(r) = \frac{q}{4 ฯ \epsilon_0} \frac{\vec r - \vec rโ}{|\vec r - \vec rโ|^3}.$$
lemma threeDimPointParticle_electricField (๐ : FreeSpace) (q : โ) (rโ : Space 3) :
(threeDimPointParticle ๐ q rโ).electricField ๐.c =
(q/ (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x : Space 3 =>
โx - rโโ ^ (- 3 : โค) โข basis.repr (x - rโ))
((IsDistBounded.zpow_smul_repr_self (- 3 : โค) (by ๐:FreeSpaceq:โrโ:Spaceโข -โ(3 - 1) - 1 โค -3 omega All goals completed! ๐)).comp_sub_right rโ)) := by ๐:FreeSpaceq:โrโ:Spaceโข (electricField ๐.c) (threeDimPointParticle ๐ q rโ) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => โx - rโโ ^ (-3) โข basis.repr (x - rโ)) โฏ)
simp only [electricField, LinearMap.coe_mk, AddHom.coe_mk, threeDimPointParticle_scalarPotential,
smul_eq_mul, threeDimPointParticle_vectorPotential, map_zero, sub_zero, Int.reduceNeg, zpow_neg] ๐:FreeSpaceq:โrโ:Spaceโข -distSpaceGrad (constantTime (distOfFunction (fun x => q / (4 * ฯ * ๐.ฮตโ) * โx - rโโโปยน) โฏ)) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)
rw [constantTime_distSpaceGrad, ๐:FreeSpaceq:โrโ:Spaceโข -constantTime (โแต (distOfFunction (fun x => q / (4 * ฯ * ๐.ฮตโ) * โx - rโโโปยน) โฏ)) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ) ๐:FreeSpaceq:โrโ:Spaceโข -constantTime (โแต ((q / (4 * ฯ * ๐.ฮตโ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ)) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ) distOfFunction_mul_fun _
(IsDistBounded.inv_shift rโ) ๐:FreeSpaceq:โrโ:Spaceโข -constantTime (โแต ((q / (4 * ฯ * ๐.ฮตโ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ)) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ) ๐:FreeSpaceq:โrโ:Spaceโข -constantTime (โแต ((q / (4 * ฯ * ๐.ฮตโ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ)) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)] ๐:FreeSpaceq:โrโ:Spaceโข -constantTime (โแต ((q / (4 * ฯ * ๐.ฮตโ)) โข distOfFunction (fun x => โx - rโโโปยน) โฏ)) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)
simp only [map_smul] ๐:FreeSpaceq:โrโ:Spaceโข -((q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (โแต (distOfFunction (fun x => โx - rโโโปยน) โฏ))) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)
trans -(q / (4 * ฯ * ๐.ฮตโ)) โข (constantTime <| distGrad <| distTranslate (basis.repr rโ) <|
(distOfFunction (fun x => โxโโปยน) (IsDistBounded.inv))) ๐:FreeSpaceq:โrโ:Spaceโข -((q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (โแต (distOfFunction (fun x => โx - rโโโปยน) โฏ))) =
-(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (โแต ((distTranslate (basis.repr rโ)) (distOfFunction (fun x => โxโโปยน) โฏ)))๐:FreeSpaceq:โrโ:Spaceโข -(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (โแต ((distTranslate (basis.repr rโ)) (distOfFunction (fun x => โxโโปยน) โฏ))) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)
ยท ๐:FreeSpaceq:โrโ:Spaceโข -((q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (โแต (distOfFunction (fun x => โx - rโโโปยน) โฏ))) =
-(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (โแต ((distTranslate (basis.repr rโ)) (distOfFunction (fun x => โxโโปยน) โฏ))) simp [distTranslate_ofFunction] All goals completed! ๐
rw [Space.distTranslate_distGrad ๐:FreeSpaceq:โrโ:Spaceโข -(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) (โแต (distOfFunction (fun x => โxโโปยน) โฏ))) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ) ๐:FreeSpaceq:โrโ:Spaceโข -(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) (โแต (distOfFunction (fun x => โxโโปยน) โฏ))) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)] ๐:FreeSpaceq:โrโ:Spaceโข -(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) (โแต (distOfFunction (fun x => โxโโปยน) โฏ))) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)
have := Space.distGrad_distOfFunction_norm_zpow (d := 3) (-1) (by ๐:FreeSpaceq:โrโ:Spaceโข -โ(3 - 1) + 1 โค -1 ๐:FreeSpaceq:โrโ:Spacethis:โแต (distOfFunction (fun x => โxโ ^ (-1)) โฏ) = distOfFunction (fun x => (โ(-1) * โxโ ^ (-1 - 2)) โข basis.repr x) โฏโข -(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) (โแต (distOfFunction (fun x => โxโโปยน) โฏ))) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ) grind All goals completed! ๐ ๐:FreeSpaceq:โrโ:Spacethis:โแต (distOfFunction (fun x => โxโ ^ (-1)) โฏ) = distOfFunction (fun x => (โ(-1) * โxโ ^ (-1 - 2)) โข basis.repr x) โฏโข -(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) (โแต (distOfFunction (fun x => โxโโปยน) โฏ))) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)) ๐:FreeSpaceq:โrโ:Spacethis:โแต (distOfFunction (fun x => โxโ ^ (-1)) โฏ) = distOfFunction (fun x => (โ(-1) * โxโ ^ (-1 - 2)) โข basis.repr x) โฏโข -(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) (โแต (distOfFunction (fun x => โxโโปยน) โฏ))) =
(q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)
simp_all [distOfFunction_neg, distTranslate_ofFunction] All goals completed! ๐C.1. the time derivative of the electric field
@[simp]
lemma threeDimPointParticle_electricField_timeDeriv (๐ : FreeSpace) (q : โ) (rโ : Space 3) :
Space.distTimeDeriv ((threeDimPointParticle ๐ q rโ).electricField ๐.c) = 0 := by ๐:FreeSpaceq:โrโ:Spaceโข distTimeDeriv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ)) = 0
rw [threeDimPointParticle_electricField, ๐:FreeSpaceq:โrโ:Spaceโข distTimeDeriv
((q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => โx - rโโ ^ (-3) โข basis.repr (x - rโ)) โฏ)) =
0 ๐:FreeSpaceq:โrโ:Spaceโข (q / (4 * ฯ * ๐.ฮตโ)) โข 0 = 0 map_smul, ๐:FreeSpaceq:โrโ:Spaceโข (q / (4 * ฯ * ๐.ฮตโ)) โข
distTimeDeriv (constantTime (distOfFunction (fun x => โx - rโโ ^ (-3) โข basis.repr (x - rโ)) โฏ)) =
0 ๐:FreeSpaceq:โrโ:Spaceโข (q / (4 * ฯ * ๐.ฮตโ)) โข 0 = 0 constantTime_distTimeDeriv ๐:FreeSpaceq:โrโ:Spaceโข (q / (4 * ฯ * ๐.ฮตโ)) โข 0 = 0 ๐:FreeSpaceq:โrโ:Spaceโข (q / (4 * ฯ * ๐.ฮตโ)) โข 0 = 0] ๐:FreeSpaceq:โrโ:Spaceโข (q / (4 * ฯ * ๐.ฮตโ)) โข 0 = 0
module All goals completed! ๐D. The magnetic field
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 ๐:FreeSpaceq:โrโ:Spaceโข (magneticFieldMatrix ๐.c) (threeDimPointParticle ๐ q rโ) = 0
ext ฮท ๐:FreeSpaceq:โrโ:Spaceฮท:๐ข(Time ร Space, โ)โข ((magneticFieldMatrix ๐.c) (threeDimPointParticle ๐ q rโ)) ฮท = 0 ฮท
simp [magneticFieldMatrix_eq_vectorPotential] All goals completed! ๐E. Maxwell's equations
The divergence of the electric field of a point particle in 3d space is given by: $$โ ยท \vec E(r) = \frac{1}{\epsilon_0} q \delta(r - rโ).$$
From this, it follows that the electromagnetic potential of a point particle in 3d space satisfies Maxwell's equations for a point particle at rest.
lemma threeDimPointParticle_div_electricField {๐} (q : โ) (rโ : Space 3) :
distSpaceDiv ((threeDimPointParticle ๐ q rโ).electricField ๐.c) =
(1/๐.ฮตโ) โข constantTime (q โข diracDelta โ rโ) := by ๐:FreeSpaceq:โrโ:Spaceโข distSpaceDiv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ)) = (1 / ๐.ฮตโ) โข constantTime (q โข diracDelta โ rโ)
rw [threeDimPointParticle_electricField ๐:FreeSpaceq:โrโ:Spaceโข distSpaceDiv ((q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => โx - rโโ ^ (-3) โข basis.repr (x - rโ)) โฏ)) =
(1 / ๐.ฮตโ) โข constantTime (q โข diracDelta โ rโ) ๐:FreeSpaceq:โrโ:Spaceโข distSpaceDiv ((q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => โx - rโโ ^ (-3) โข basis.repr (x - rโ)) โฏ)) =
(1 / ๐.ฮตโ) โข constantTime (q โข diracDelta โ rโ)] ๐:FreeSpaceq:โrโ:Spaceโข distSpaceDiv ((q / (4 * ฯ * ๐.ฮตโ)) โข constantTime (distOfFunction (fun x => โx - rโโ ^ (-3) โข basis.repr (x - rโ)) โฏ)) =
(1 / ๐.ฮตโ) โข constantTime (q โข diracDelta โ rโ)
simp only [Int.reduceNeg, zpow_neg, map_smul, smul_smul] ๐:FreeSpaceq:โrโ:Spaceโข (q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv (constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)) =
(1 / ๐.ฮตโ * q) โข constantTime (diracDelta โ rโ)
have h1 := Space.distDiv_inv_pow_eq_dim (d := 3) ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => โxโ ^ (-โ3) โข basis.repr x) โฏ) = (โ3 * volume.real (Metric.ball 0 1)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv (constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)) =
(1 / ๐.ฮตโ * q) โข constantTime (diracDelta โ rโ)
simp at h1 ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv (constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)) =
(1 / ๐.ฮตโ * q) โข constantTime (diracDelta โ rโ)
trans (q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv (constantTime <|
distTranslate (basis.repr rโ) <|
(distOfFunction (fun x => โxโ ^ (-3 : โค) โข basis.repr x)
(IsDistBounded.zpow_smul_repr_self (- 3 : โค) (by ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข -โ(3 - 1) - 1 โค -3 omega All goals completed! ๐))))
ยท ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv (constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)) =
(q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv
(constantTime ((distTranslate (basis.repr rโ)) (distOfFunction (fun x => โxโ ^ (-3) โข basis.repr x) โฏ))) ext ฮท ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0ฮท:๐ข(Time ร Space, โ)โข ((q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv (constantTime (distOfFunction (fun x => (โx - rโโ ^ 3)โปยน โข basis.repr (x - rโ)) โฏ)))
ฮท =
((q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv
(constantTime ((distTranslate (basis.repr rโ)) (distOfFunction (fun x => โxโ ^ (-3) โข basis.repr x) โฏ))))
ฮท
simp [distTranslate_ofFunction] All goals completed! ๐
simp only [Int.reduceNeg, zpow_neg, one_div] ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข
distSpaceDiv
(constantTime ((distTranslate (basis.repr rโ)) (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ))) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ)
rw [constantTime_distSpaceDiv, ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข
constantTime (distDiv ((distTranslate (basis.repr rโ)) (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ))) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ) ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) ((3 * (4 / 3 * ฯ)) โข diracDelta โ 0)) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ) distDiv_distTranslate, ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข
constantTime ((distTranslate (basis.repr rโ)) (distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ))) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ) ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) ((3 * (4 / 3 * ฯ)) โข diracDelta โ 0)) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ) h1 ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) ((3 * (4 / 3 * ฯ)) โข diracDelta โ 0)) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ) ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) ((3 * (4 / 3 * ฯ)) โข diracDelta โ 0)) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ)] ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ)) โข constantTime ((distTranslate (basis.repr rโ)) ((3 * (4 / 3 * ฯ)) โข diracDelta โ 0)) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ)
simp only [map_smul, smul_smul] ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0โข (q / (4 * ฯ * ๐.ฮตโ) * (3 * (4 / 3 * ฯ))) โข constantTime ((distTranslate (basis.repr rโ)) (diracDelta โ 0)) =
(๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ)
ext ฮท ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0ฮท:๐ข(Time ร Space, โ)โข ((q / (4 * ฯ * ๐.ฮตโ) * (3 * (4 / 3 * ฯ))) โข constantTime ((distTranslate (basis.repr rโ)) (diracDelta โ 0))) ฮท =
((๐.ฮตโโปยน * q) โข constantTime (diracDelta โ rโ)) ฮท
simp [constantTime_apply, diracDelta_apply, distTranslate_apply] ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0ฮท:๐ข(Time ร Space, โ)โข q / (4 * ฯ * ๐.ฮตโ) * (3 * (4 / 3 * ฯ)) = ๐.ฮตโโปยน * q โจ (timeIntegralSchwartz ฮท) rโ = 0
left ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0ฮท:๐ข(Time ร Space, โ)โข q / (4 * ฯ * ๐.ฮตโ) * (3 * (4 / 3 * ฯ)) = ๐.ฮตโโปยน * q
ring_nf ๐:FreeSpaceq:โrโ:Spaceh1:distDiv (distOfFunction (fun x => (โxโ ^ 3)โปยน โข basis.repr x) โฏ) = (3 * (4 / 3 * ฯ)) โข diracDelta โ 0ฮท:๐ข(Time ร Space, โ)โข q * ฯ * ฯโปยน * ๐.ฮตโโปยน = q * ๐.ฮตโโปยน
field_simp All goals completed! ๐
lemma threeDimPointParticle_isExterma (๐ : FreeSpace) (q : โ) (rโ : Space 3) :
(threeDimPointParticle ๐ q rโ).IsExtrema ๐ (threeDimPointParticleCurrentDensity ๐.c q rโ) := by ๐:FreeSpaceq:โrโ:Spaceโข IsExtrema ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)
rw [isExtrema_iff_components ๐:FreeSpaceq:โrโ:Spaceโข (โ (ฮต : ๐ข(SpaceTime, โ)),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inl 0) =
0) โง
โ (ฮต : ๐ข(SpaceTime, โ)) (i : Fin 3),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inr i) = 0 ๐:FreeSpaceq:โrโ:Spaceโข (โ (ฮต : ๐ข(SpaceTime, โ)),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inl 0) =
0) โง
โ (ฮต : ๐ข(SpaceTime, โ)) (i : Fin 3),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inr i) = 0] ๐:FreeSpaceq:โrโ:Spaceโข (โ (ฮต : ๐ข(SpaceTime, โ)),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inl 0) =
0) โง
โ (ฮต : ๐ข(SpaceTime, โ)) (i : Fin 3),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inr i) = 0
apply And.intro left ๐:FreeSpaceq:โrโ:Spaceโข โ (ฮต : ๐ข(SpaceTime, โ)),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inl 0) = 0right ๐:FreeSpaceq:โrโ:Spaceโข โ (ฮต : ๐ข(SpaceTime, โ)) (i : Fin 3),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inr i) = 0
ยท left ๐:FreeSpaceq:โrโ:Spaceโข โ (ฮต : ๐ข(SpaceTime, โ)),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inl 0) = 0 intro ฮต left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข (gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inl 0) = 0
rw [gradLagrangian_sum_inl_0 left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข 1 / (๐.ฮผโ * ๐.c.val) *
((SpaceTime.distTimeSlice ๐.c).symm (distSpaceDiv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ)))) ฮต -
๐.c.val *
((SpaceTime.distTimeSlice ๐.c).symm
((DistLorentzCurrentDensity.chargeDensity ๐.c) (threeDimPointParticleCurrentDensity ๐.c q rโ)))
ฮต =
0 left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข 1 / (๐.ฮผโ * ๐.c.val) *
((SpaceTime.distTimeSlice ๐.c).symm (distSpaceDiv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ)))) ฮต -
๐.c.val *
((SpaceTime.distTimeSlice ๐.c).symm
((DistLorentzCurrentDensity.chargeDensity ๐.c) (threeDimPointParticleCurrentDensity ๐.c q rโ)))
ฮต =
0]left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข 1 / (๐.ฮผโ * ๐.c.val) *
((SpaceTime.distTimeSlice ๐.c).symm (distSpaceDiv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ)))) ฮต -
๐.c.val *
((SpaceTime.distTimeSlice ๐.c).symm
((DistLorentzCurrentDensity.chargeDensity ๐.c) (threeDimPointParticleCurrentDensity ๐.c q rโ)))
ฮต =
0
simp only [one_div, mul_inv_rev, threeDimPointParticleCurrentDensity_chargeDensity, map_smul,
FunLike.coe_smul, Pi.smul_apply, smul_eq_mul] left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข ๐.c.valโปยน * ๐.ฮผโโปยน *
((SpaceTime.distTimeSlice ๐.c).symm (distSpaceDiv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ)))) ฮต -
๐.c.val * (q * ((SpaceTime.distTimeSlice ๐.c).symm (constantTime (diracDelta โ rโ))) ฮต) =
0
rw [threeDimPointParticle_div_electricField left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข ๐.c.valโปยน * ๐.ฮผโโปยน * ((SpaceTime.distTimeSlice ๐.c).symm ((1 / ๐.ฮตโ) โข constantTime (q โข diracDelta โ rโ))) ฮต -
๐.c.val * (q * ((SpaceTime.distTimeSlice ๐.c).symm (constantTime (diracDelta โ rโ))) ฮต) =
0 left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข ๐.c.valโปยน * ๐.ฮผโโปยน * ((SpaceTime.distTimeSlice ๐.c).symm ((1 / ๐.ฮตโ) โข constantTime (q โข diracDelta โ rโ))) ฮต -
๐.c.val * (q * ((SpaceTime.distTimeSlice ๐.c).symm (constantTime (diracDelta โ rโ))) ฮต) =
0]left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข ๐.c.valโปยน * ๐.ฮผโโปยน * ((SpaceTime.distTimeSlice ๐.c).symm ((1 / ๐.ฮตโ) โข constantTime (q โข diracDelta โ rโ))) ฮต -
๐.c.val * (q * ((SpaceTime.distTimeSlice ๐.c).symm (constantTime (diracDelta โ rโ))) ฮต) =
0
simp only [one_div, map_smul, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul] left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข ๐.c.valโปยน * ๐.ฮผโโปยน * (๐.ฮตโโปยน * (q * ((SpaceTime.distTimeSlice ๐.c).symm (constantTime (diracDelta โ rโ))) ฮต)) -
๐.c.val * (q * ((SpaceTime.distTimeSlice ๐.c).symm (constantTime (diracDelta โ rโ))) ฮต) =
0
field_simp left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข q * ((SpaceTime.distTimeSlice ๐.c).symm (constantTime (diracDelta โ rโ))) ฮต * (1 - ๐.c.val ^ 2 * ๐.ฮผโ * ๐.ฮตโ) =
๐.c.val * ๐.ฮผโ * ๐.ฮตโ * 0
simp [๐.c_sq] left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข (q = 0 โจ ((SpaceTime.distTimeSlice ๐.c).symm (constantTime (diracDelta โ rโ))) ฮต = 0) โจ
1 - ๐.ฮผโโปยน * ๐.ฮตโโปยน * ๐.ฮผโ * ๐.ฮตโ = 0
right left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข 1 - ๐.ฮผโโปยน * ๐.ฮตโโปยน * ๐.ฮผโ * ๐.ฮตโ = 0
field_simp left ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)โข 1 - 1 = 0
simp All goals completed! ๐
ยท right ๐:FreeSpaceq:โrโ:Spaceโข โ (ฮต : ๐ข(SpaceTime, โ)) (i : Fin 3),
(gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inr i) = 0 intro ฮต i right ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)i:Fin 3โข (gradLagrangian ๐ (threeDimPointParticle ๐ q rโ) (threeDimPointParticleCurrentDensity ๐.c q rโ)) ฮต (Sum.inr i) = 0
rw [gradLagrangian_sum_inr_i right ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)i:Fin 3โข ๐.ฮผโโปยน *
(1 / ๐.c.val ^ 2 *
(((SpaceTime.distTimeSlice ๐.c).symm (distTimeDeriv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ))))
ฮต).ofLp
i -
โ j,
(((PiLp.basisFun 2 โ (Fin 3)).tensorProduct (PiLp.basisFun 2 โ (Fin 3))).repr
(((SpaceTime.distTimeSlice ๐.c).symm
((distSpaceDeriv j) ((magneticFieldMatrix ๐.c) (threeDimPointParticle ๐ q rโ))))
ฮต))
(j, i)) +
(((SpaceTime.distTimeSlice ๐.c).symm
((DistLorentzCurrentDensity.currentDensity ๐.c) (threeDimPointParticleCurrentDensity ๐.c q rโ)))
ฮต).ofLp
i =
0 right ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)i:Fin 3โข ๐.ฮผโโปยน *
(1 / ๐.c.val ^ 2 *
(((SpaceTime.distTimeSlice ๐.c).symm (distTimeDeriv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ))))
ฮต).ofLp
i -
โ j,
(((PiLp.basisFun 2 โ (Fin 3)).tensorProduct (PiLp.basisFun 2 โ (Fin 3))).repr
(((SpaceTime.distTimeSlice ๐.c).symm
((distSpaceDeriv j) ((magneticFieldMatrix ๐.c) (threeDimPointParticle ๐ q rโ))))
ฮต))
(j, i)) +
(((SpaceTime.distTimeSlice ๐.c).symm
((DistLorentzCurrentDensity.currentDensity ๐.c) (threeDimPointParticleCurrentDensity ๐.c q rโ)))
ฮต).ofLp
i =
0]right ๐:FreeSpaceq:โrโ:Spaceฮต:๐ข(SpaceTime, โ)i:Fin 3โข ๐.ฮผโโปยน *
(1 / ๐.c.val ^ 2 *
(((SpaceTime.distTimeSlice ๐.c).symm (distTimeDeriv ((electricField ๐.c) (threeDimPointParticle ๐ q rโ))))
ฮต).ofLp
i -
โ j,
(((PiLp.basisFun 2 โ (Fin 3)).tensorProduct (PiLp.basisFun 2 โ (Fin 3))).repr
(((SpaceTime.distTimeSlice ๐.c).symm
((distSpaceDeriv j) ((magneticFieldMatrix ๐.c) (threeDimPointParticle ๐ q rโ))))
ฮต))
(j, i)) +
(((SpaceTime.distTimeSlice ๐.c).symm
((DistLorentzCurrentDensity.currentDensity ๐.c) (threeDimPointParticleCurrentDensity ๐.c q rโ)))
ฮต).ofLp
i =
0
simp All goals completed! ๐