Physlib.Electromagnetism.PointParticle.OneDimension — Physlib

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.Translations

The electrostatics of a stationary point particle in 1d

i. Overview

In this module we give the electromagnetic properties of a point particle sitting at the origin in 1d space.

ii. Key results

oneDimPointParticle : The electromagnetic potential of a point particle stationary at the origin of 1d space.

oneDimPointParticle_isExterma : The electric field of a point particle stationary at the origin of 1d space satisfies Maxwell's equations

iii. Table of contents

A. The current density

B. The Potentials

B.1. The electromagnetic potential

B.2. The vector potential is zero

B.3. The scalar potential

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 section

A. The current density

              

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)))) := byc:SpeedOfLightq:ℝr₀:Space 1⊢ oneDimPointParticleCurrentDensity c q r₀ =
  (SpaceTime.distTimeSlice c).symm
    (constantTime ((distTranslate (basis.repr r₀)) ((c.val * q) • diracDelta' ℝ 0 (Lorentz.Vector.basis (Sum.inl 0)))))
  rw [oneDimPointParticleCurrentDensityc:SpeedOfLightq:ℝr₀:Space 1⊢ (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)))))c:SpeedOfLightq:ℝr₀:Space 1⊢ (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)))))]c:SpeedOfLightq:ℝr₀:Space 1⊢ (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)))))
  congre_6.e_6c:SpeedOfLightq:ℝr₀:Space 1⊢ (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_6c:SpeedOfLightq:ℝr₀:Space 1η:𝓢(Space 1, ℝ)i✝:Fin 1 ⊕ Fin 1⊢ ((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! 🐙@[simp]
lemma oneDimPointParticleCurrentDensity_currentDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) :
    (oneDimPointParticleCurrentDensity c q r₀).currentDensity c = 0 := byc:SpeedOfLightq:ℝr₀:Space 1⊢ (DistLorentzCurrentDensity.currentDensity c) (oneDimPointParticleCurrentDensity c q r₀) = 0
  ext ε ic:SpeedOfLightq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)i:Fin 1⊢ (((DistLorentzCurrentDensity.currentDensity c) (oneDimPointParticleCurrentDensity c q r₀)) ε).ofLp i = (0 ε).ofLp i
  simp [oneDimPointParticleCurrentDensity, DistLorentzCurrentDensity.currentDensity,
    Lorentz.Vector.spatialCLM, constantTime_apply]All goals completed! 🐙@[simp]
lemma oneDimPointParticleCurrentDensity_chargeDensity (c : SpeedOfLight) (q : ℝ) (r₀ : Space 1) :
    (oneDimPointParticleCurrentDensity c q r₀).chargeDensity c =
    constantTime (q • diracDelta ℝ r₀) := byc:SpeedOfLightq:ℝr₀:Space 1⊢ (DistLorentzCurrentDensity.chargeDensity c) (oneDimPointParticleCurrentDensity c q r₀) =
  constantTime (q • diracDelta ℝ r₀)
  ext εc:SpeedOfLightq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ ((DistLorentzCurrentDensity.chargeDensity c) (oneDimPointParticleCurrentDensity c q r₀)) ε =
  (constantTime (q • diracDelta ℝ r₀)) ε
  simp only [DistLorentzCurrentDensity.chargeDensity, one_div, Lorentz.Vector.temporalCLM,
    Fin.isValue, oneDimPointParticleCurrentDensity, 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 1ε:𝓢(Time × Space 1, ℝ)⊢ c.val * q * (c.val⁻¹ * (timeIntegralSchwartz ε) r₀) = q * (timeIntegralSchwartz ε) r₀
  field_simpAll goals completed! 🐙

B. The Potentials

B.1. The electromagnetic potential



lemma oneDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
    oneDimPointParticle 𝓕 q r₀ = ((SpaceTime.distTimeSlice 𝓕.c).symm <|
    constantTime <|
    distTranslate (basis.repr r₀) <|
    distOfFunction (fun x => ((- (q * 𝓕.μ₀ * 𝓕.c)/ 2) * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0))
      (by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ IsDistBounded fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0) fun_propAll goals completed! 🐙)) := by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ oneDimPointParticle 𝓕 q r₀ =
  (SpaceTime.distTimeSlice 𝓕.c).symm
    (constantTime
      ((distTranslate (basis.repr r₀))
        (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)))
  rw [oneDimPointParticle𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (SpaceTime.distTimeSlice 𝓕.c).symm
    (constantTime
      (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)) =
  (SpaceTime.distTimeSlice 𝓕.c).symm
    (constantTime
      ((distTranslate (basis.repr r₀))
        (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)))𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (SpaceTime.distTimeSlice 𝓕.c).symm
    (constantTime
      (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)) =
  (SpaceTime.distTimeSlice 𝓕.c).symm
    (constantTime
      ((distTranslate (basis.repr r₀))
        (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)))]𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (SpaceTime.distTimeSlice 𝓕.c).symm
    (constantTime
      (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)) =
  (SpaceTime.distTimeSlice 𝓕.c).symm
    (constantTime
      ((distTranslate (basis.repr r₀))
        (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)))
  congre_6.e_6𝓕:FreeSpaceq:ℝr₀:Space 1⊢ distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯ =
  (distTranslate (basis.repr r₀))
    (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯)
  ext ηe_6.e_6𝓕:FreeSpaceq:ℝr₀:Space 1η:𝓢(Space 1, ℝ)i✝:Fin 1 ⊕ Fin 1⊢ (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x - r₀‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯) η i✝ =
  ((distTranslate (basis.repr r₀))
      (distOfFunction (fun x => (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x‖) • Lorentz.Vector.basis (Sum.inl 0)) ⋯))
    η i✝
  simp [distTranslate_ofFunction]All goals completed! 🐙

/-

### B.2. The vector potential is zero

-/

@[simp]
lemma oneDimPointParticle_vectorPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
    (oneDimPointParticle 𝓕 q r₀).vectorPotential 𝓕.c = 0 := by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (vectorPotential 𝓕.c) (oneDimPointParticle 𝓕 q r₀) = 0
  ext ε i𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)i:Fin 1⊢ (((vectorPotential 𝓕.c) (oneDimPointParticle 𝓕 q r₀)) ε).ofLp i = (0 ε).ofLp i
  simp [vectorPotential, Lorentz.Vector.spatialCLM,
    oneDimPointParticle, constantTime_apply, distOfFunction_vector_eval]All goals completed! 🐙

B.3. The scalar potential



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𝓕:FreeSpaceq:ℝr₀:Space 1⊢ IsDistBounded fun x => -(q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • ‖x - r₀‖ fun_propAll goals completed! 🐙)) := by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (scalarPotential 𝓕.c) (oneDimPointParticle 𝓕 q r₀) =
  constantTime (distOfFunction (fun x => -(q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • ‖x - r₀‖) ⋯)
  ext ε𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ ((scalarPotential 𝓕.c) (oneDimPointParticle 𝓕 q r₀)) ε =
  (constantTime (distOfFunction (fun x => -(q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • ‖x - r₀‖) ⋯)) ε
  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, 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, neg_mul]𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * (distOfFunction (fun x => -(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε) =
  (distOfFunction (fun x => -(q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2 * ‖x - r₀‖)) ⋯) (timeIntegralSchwartz ε)
  rw [distOfFunction_mul_fun _ (by𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ IsDistBounded fun x => ‖x - r₀‖𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * ((-(q * 𝓕.μ₀ * 𝓕.c.val) / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε) =
  (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯)) (timeIntegralSchwartz ε) fun_propAll goals completed! 🐙𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * ((-(q * 𝓕.μ₀ * 𝓕.c.val) / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε) =
  (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯)) (timeIntegralSchwartz ε)), distOfFunction_neg,𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * ((-(q * 𝓕.μ₀ * 𝓕.c.val) / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε) =
  (-distOfFunction (fun x => q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2 * ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε)𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * ((-(q * 𝓕.μ₀ * 𝓕.c.val) / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε) =
  (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯)) (timeIntegralSchwartz ε)
    distOfFunction_mul_fun _ (by𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ IsDistBounded fun x => ‖x - r₀‖𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * ((-(q * 𝓕.μ₀ * 𝓕.c.val) / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε) =
  (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯)) (timeIntegralSchwartz ε) fun_propAll goals completed! 🐙𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * ((-(q * 𝓕.μ₀ * 𝓕.c.val) / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε) =
  (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯)) (timeIntegralSchwartz ε))]𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * ((-(q * 𝓕.μ₀ * 𝓕.c.val) / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε) =
  (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯)) (timeIntegralSchwartz ε)
  simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul,
    _root_.neg_apply]𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(Time × Space 1, ℝ)⊢ 𝓕.c.val * (-(q * 𝓕.μ₀ * 𝓕.c.val) / 2 * (distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε)) =
  -(q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2 * (distOfFunction (fun x => ‖x - r₀‖) ⋯) (timeIntegralSchwartz ε))
  ringAll goals completed! 🐙

C. The electric field



lemma oneDimPointParticle_electricField (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
    (oneDimPointParticle 𝓕 q r₀).electricField 𝓕.c =
    ((q * 𝓕.μ₀ * 𝓕.c ^ 2) / 2) • constantTime (distOfFunction (fun x : Space 1 =>
      ‖x - r₀‖ ^ (- 1 : ℤ) • basis.repr (x - r₀))
      ((IsDistBounded.zpow_smul_repr_self (- 1 : ℤ) (by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ -↑(1 - 1) - 1 ≤ -1 omegaAll goals completed! 🐙)).comp_sub_right r₀)) := by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯)
  have h1 := Space.distGrad_distOfFunction_norm_zpow (d := 1) 1 (by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ -↑(1 - 1) + 1 ≤ 1𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) = distOfFunction (fun x => (↑1 * ‖x‖ ^ (1 - 2)) • basis.repr x) ⋯⊢ (electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯) grindAll goals completed! 🐙𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) = distOfFunction (fun x => (↑1 * ‖x‖ ^ (1 - 2)) • basis.repr x) ⋯⊢ (electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯))𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖ ^ 1) ⋯) = distOfFunction (fun x => (↑1 * ‖x‖ ^ (1 - 2)) • basis.repr x) ⋯⊢ (electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯)
  simp at h1𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ (electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯)
  simp only [electricField, LinearMap.coe_mk, AddHom.coe_mk, oneDimPointParticle_scalarPotential,
    smul_eq_mul, neg_mul, oneDimPointParticle_vectorPotential, map_zero, sub_zero, Int.reduceNeg,
    zpow_neg, zpow_one]𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ -distSpaceGrad (constantTime (distOfFunction (fun x => -(q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2 * ‖x - r₀‖)) ⋯)) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)
  rw [constantTime_distSpaceGrad,𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ -constantTime (∇ᵈ (distOfFunction (fun x => -(q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2 * ‖x - r₀‖)) ⋯)) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ -constantTime (∇ᵈ (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯))) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯) distOfFunction_neg,𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ -constantTime (∇ᵈ (-distOfFunction (fun x => q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2 * ‖x - r₀‖) ⋯)) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ -constantTime (∇ᵈ (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯))) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯) distOfFunction_mul_fun _ (by𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ IsDistBounded fun x => ‖x - r₀‖𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ -constantTime (∇ᵈ (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯))) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯) fun_propAll goals completed! 🐙𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ -constantTime (∇ᵈ (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯))) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯))]𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ -constantTime (∇ᵈ (-((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • distOfFunction (fun x => ‖x - r₀‖) ⋯))) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)
  simp only [map_neg, map_smul, neg_neg]𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (∇ᵈ (distOfFunction (fun x => ‖x - r₀‖) ⋯)) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)
  congre_a.e_6𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ ∇ᵈ (distOfFunction (fun x => ‖x - r₀‖) ⋯) = distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯
  trans distGrad <| distTranslate (basis.repr r₀) <| (distOfFunction (fun x => ‖x‖) (by𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ IsDistBounded fun x => ‖x‖ fun_propAll goals completed! 🐙))
  ·𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ ∇ᵈ (distOfFunction (fun x => ‖x - r₀‖) ⋯) = ∇ᵈ ((distTranslate (basis.repr r₀)) (distOfFunction (fun x => ‖x‖) ⋯)) ext1 η𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯η:𝓢(Space 1, ℝ)⊢ (∇ᵈ (distOfFunction (fun x => ‖x - r₀‖) ⋯)) η =
  (∇ᵈ ((distTranslate (basis.repr r₀)) (distOfFunction (fun x => ‖x‖) ⋯))) η
    simp [distTranslate_ofFunction]All goals completed! 🐙
  rw [Space.distTranslate_distGrad𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ (distTranslate (basis.repr r₀)) (∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯)) =
  distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ (distTranslate (basis.repr r₀)) (∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯)) =
  distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯]𝓕:FreeSpaceq:ℝr₀:Space 1h1:∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯) = distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯⊢ (distTranslate (basis.repr r₀)) (∇ᵈ (distOfFunction (fun x => ‖x‖) ⋯)) =
  distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯
  simp [h1, distTranslate_ofFunction]All goals completed! 🐙

C.1. The time derivative of the electric field



@[simp]
lemma oneDimPointParticle_electricField_timeDeriv (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
    Space.distTimeDeriv ((oneDimPointParticle 𝓕 q r₀).electricField 𝓕.c) = 0 := by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ distTimeDeriv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀)) = 0
  rw [oneDimPointParticle_electricField,𝓕:FreeSpaceq:ℝr₀:Space 1⊢ distTimeDeriv
    ((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯)) =
  0𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • 0 = 0 map_smul,𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    distTimeDeriv (constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯)) =
  0𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • 0 = 0 constantTime_distTimeDeriv𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • 0 = 0𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • 0 = 0]𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • 0 = 0
  moduleAll goals completed! 🐙

D. The magnetic field

lemma oneDimPointParticle_magneticFieldMatrix (q : ℝ) (r₀ : Space 1) :
    (oneDimPointParticle 𝓕 q r₀).magneticFieldMatrix 𝓕.c = 0 := by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (magneticFieldMatrix 𝓕.c) (oneDimPointParticle 𝓕 q r₀) = 0
  simpAll goals completed! 🐙

E. Maxwell's equations



lemma oneDimPointParticle_div_electricField {𝓕} (q : ℝ) (r₀ : Space 1) :
    distSpaceDiv ((oneDimPointParticle 𝓕 q r₀).electricField 𝓕.c) =
    (𝓕.μ₀ * 𝓕.c ^ 2) • constantTime (q • diracDelta ℝ r₀) := by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ distSpaceDiv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime (q • diracDelta ℝ r₀)
  rw [oneDimPointParticle_electricField𝓕:FreeSpaceq:ℝr₀:Space 1⊢ distSpaceDiv
    ((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime (q • diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1⊢ distSpaceDiv
    ((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime (q • diracDelta ℝ r₀)]𝓕:FreeSpaceq:ℝr₀:Space 1⊢ distSpaceDiv
    ((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • constantTime (distOfFunction (fun x => ‖x - r₀‖ ^ (-1) • basis.repr (x - r₀)) ⋯)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime (q • diracDelta ℝ r₀)
  simp only [Int.reduceNeg, zpow_neg, zpow_one, map_smul, smul_smul]𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    distSpaceDiv (constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)
  have h1 := Space.distDiv_inv_pow_eq_dim (d := 1)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖ ^ (-↑1) • basis.repr x) ⋯) = (↑1 * volume.real (Metric.ball 0 1)) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    distSpaceDiv (constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)
  simp at h1𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    distSpaceDiv (constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)
  trans (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    distSpaceDiv (constantTime <|
    distTranslate (basis.repr r₀) <|
    (distOfFunction (fun x => ‖x‖ ^ (-1 : ℤ) • basis.repr x)
      (IsDistBounded.zpow_smul_repr_self (- 1 : ℤ) (by𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ -↑(1 - 1) - 1 ≤ -1 omegaAll goals completed! 🐙))))
  ·𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    distSpaceDiv (constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)) =
  (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    distSpaceDiv
      (constantTime ((distTranslate (basis.repr r₀)) (distOfFunction (fun x => ‖x‖ ^ (-1) • basis.repr x) ⋯))) ext η𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0η:𝓢(Time × Space 1, ℝ)⊢ ((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
      distSpaceDiv (constantTime (distOfFunction (fun x => ‖x - r₀‖⁻¹ • basis.repr (x - r₀)) ⋯)))
    η =
  ((q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
      distSpaceDiv
        (constantTime ((distTranslate (basis.repr r₀)) (distOfFunction (fun x => ‖x‖ ^ (-1) • basis.repr x) ⋯))))
    η
    simp [distTranslate_ofFunction]All goals completed! 🐙
  simp only [Int.reduceNeg, zpow_neg, zpow_one]𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    distSpaceDiv (constantTime ((distTranslate (basis.repr r₀)) (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯))) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)
  rw [constantTime_distSpaceDiv,𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    constantTime (distDiv ((distTranslate (basis.repr r₀)) (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯))) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    constantTime ((distTranslate (basis.repr r₀)) (volume.real (Metric.ball 0 1) • diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀) distDiv_distTranslate,𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    constantTime ((distTranslate (basis.repr r₀)) (distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯))) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    constantTime ((distTranslate (basis.repr r₀)) (volume.real (Metric.ball 0 1) • diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀) h1𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    constantTime ((distTranslate (basis.repr r₀)) (volume.real (Metric.ball 0 1) • diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    constantTime ((distTranslate (basis.repr r₀)) (volume.real (Metric.ball 0 1) • diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)]𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    constantTime ((distTranslate (basis.repr r₀)) (volume.real (Metric.ball 0 1) • diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)
  simp only [map_smul]𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    volume.real (Metric.ball 0 1) • constantTime ((distTranslate (basis.repr r₀)) (diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)
  suffices h : volume.real (Metric.ball (0 : Space 1) 1) = 2 by𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0h:volume.real (Metric.ball 0 1) = 2⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) •
    volume.real (Metric.ball 0 1) • constantTime ((distTranslate (basis.repr r₀)) (diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2
    rw [h𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0h:volume.real (Metric.ball 0 1) = 2⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • 2 • constantTime ((distTranslate (basis.repr r₀)) (diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0h:volume.real (Metric.ball 0 1) = 2⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • 2 • constantTime ((distTranslate (basis.repr r₀)) (diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2]𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0h:volume.real (Metric.ball 0 1) = 2⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2 / 2) • 2 • constantTime ((distTranslate (basis.repr r₀)) (diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2
    simp [smul_smul]𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0h:volume.real (Metric.ball 0 1) = 2⊢ (q * 𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime ((distTranslate (basis.repr r₀)) (diracDelta ℝ 0)) =
  (𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2
    ext η𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0h:volume.real (Metric.ball 0 1) = 2η:𝓢(Time × Space 1, ℝ)⊢ ((q * 𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime ((distTranslate (basis.repr r₀)) (diracDelta ℝ 0))) η =
  ((𝓕.μ₀ * 𝓕.c.val ^ 2 * q) • constantTime (diracDelta ℝ r₀)) η𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2
    simp [constantTime_apply, diracDelta_apply, distTranslate_apply]𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0h:volume.real (Metric.ball 0 1) = 2η:𝓢(Time × Space 1, ℝ)⊢ q * 𝓕.μ₀ * 𝓕.c.val ^ 2 = 𝓕.μ₀ * 𝓕.c.val ^ 2 * q ∨ (timeIntegralSchwartz η) r₀ = 0𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2
    left𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0h:volume.real (Metric.ball 0 1) = 2η:𝓢(Time × Space 1, ℝ)⊢ q * 𝓕.μ₀ * 𝓕.c.val ^ 2 = 𝓕.μ₀ * 𝓕.c.val ^ 2 * q𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2
    ring_nf𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ volume.real (Metric.ball 0 1) = 2
  simp [MeasureTheory.Measure.real]𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (volume (Metric.ball 0 1)).toReal = 2
  rw [InnerProductSpace.volume_ball_of_dim_odd (k := 0)𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (ENNReal.ofReal 1 ^ Module.finrank ℝ (Space 1) *
      ENNReal.ofReal (Real.pi ^ 0 * 2 ^ (0 + 1) / ↑(Module.finrank ℝ (Space 1)).doubleFactorial)).toReal =
  2hk𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ Module.finrank ℝ (Space 1) = 2 * 0 + 1𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (ENNReal.ofReal 1 ^ Module.finrank ℝ (Space 1) *
      ENNReal.ofReal (Real.pi ^ 0 * 2 ^ (0 + 1) / ↑(Module.finrank ℝ (Space 1)).doubleFactorial)).toReal =
  2hk𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ Module.finrank ℝ (Space 1) = 2 * 0 + 1]𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (ENNReal.ofReal 1 ^ Module.finrank ℝ (Space 1) *
      ENNReal.ofReal (Real.pi ^ 0 * 2 ^ (0 + 1) / ↑(Module.finrank ℝ (Space 1)).doubleFactorial)).toReal =
  2hk𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ Module.finrank ℝ (Space 1) = 2 * 0 + 1
  ·𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ (ENNReal.ofReal 1 ^ Module.finrank ℝ (Space 1) *
      ENNReal.ofReal (Real.pi ^ 0 * 2 ^ (0 + 1) / ↑(Module.finrank ℝ (Space 1)).doubleFactorial)).toReal =
  2 simpAll goals completed! 🐙
  ·hk𝓕:FreeSpaceq:ℝr₀:Space 1h1:distDiv (distOfFunction (fun x => ‖x‖⁻¹ • basis.repr x) ⋯) = volume.real (Metric.ball 0 1) • diracDelta ℝ 0⊢ Module.finrank ℝ (Space 1) = 2 * 0 + 1 simpAll goals completed! 🐙



lemma oneDimPointParticle_isExterma (𝓕 : FreeSpace) (q : ℝ) (r₀ : Space 1) :
    (oneDimPointParticle 𝓕 q r₀).IsExtrema 𝓕 (oneDimPointParticleCurrentDensity 𝓕.c q r₀) := by𝓕:FreeSpaceq:ℝr₀:Space 1⊢ IsExtrema 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)
  rw [isExtrema_iff_components𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (∀ (ε : 𝓢(SpaceTime 1, ℝ)),
    (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inl 0) = 0) ∧
  ∀ (ε : 𝓢(SpaceTime 1, ℝ)) (i : Fin 1),
    (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inr i) = 0𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (∀ (ε : 𝓢(SpaceTime 1, ℝ)),
    (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inl 0) = 0) ∧
  ∀ (ε : 𝓢(SpaceTime 1, ℝ)) (i : Fin 1),
    (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inr i) = 0]𝓕:FreeSpaceq:ℝr₀:Space 1⊢ (∀ (ε : 𝓢(SpaceTime 1, ℝ)),
    (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inl 0) = 0) ∧
  ∀ (ε : 𝓢(SpaceTime 1, ℝ)) (i : Fin 1),
    (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inr i) = 0
  apply And.introleft𝓕:FreeSpaceq:ℝr₀:Space 1⊢ ∀ (ε : 𝓢(SpaceTime 1, ℝ)),
  (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inl 0) = 0right𝓕:FreeSpaceq:ℝr₀:Space 1⊢ ∀ (ε : 𝓢(SpaceTime 1, ℝ)) (i : Fin 1),
  (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inr i) = 0
  ·left𝓕:FreeSpaceq:ℝr₀:Space 1⊢ ∀ (ε : 𝓢(SpaceTime 1, ℝ)),
  (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inl 0) = 0 intro εleft𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inl 0) = 0
    rw [gradLagrangian_sum_inl_0left𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 1 / (𝓕.μ₀ * 𝓕.c.val) *
      ((SpaceTime.distTimeSlice 𝓕.c).symm (distSpaceDiv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀)))) ε -
    𝓕.c.val *
      ((SpaceTime.distTimeSlice 𝓕.c).symm
          ((DistLorentzCurrentDensity.chargeDensity 𝓕.c) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)))
        ε =
  0left𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 1 / (𝓕.μ₀ * 𝓕.c.val) *
      ((SpaceTime.distTimeSlice 𝓕.c).symm (distSpaceDiv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀)))) ε -
    𝓕.c.val *
      ((SpaceTime.distTimeSlice 𝓕.c).symm
          ((DistLorentzCurrentDensity.chargeDensity 𝓕.c) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)))
        ε =
  0]left𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 1 / (𝓕.μ₀ * 𝓕.c.val) *
      ((SpaceTime.distTimeSlice 𝓕.c).symm (distSpaceDiv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀)))) ε -
    𝓕.c.val *
      ((SpaceTime.distTimeSlice 𝓕.c).symm
          ((DistLorentzCurrentDensity.chargeDensity 𝓕.c) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)))
        ε =
  0
    simp only [one_div, mul_inv_rev, oneDimPointParticleCurrentDensity_chargeDensity, map_smul,
      FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]left𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
      ((SpaceTime.distTimeSlice 𝓕.c).symm (distSpaceDiv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀)))) ε -
    𝓕.c.val * (q * ((SpaceTime.distTimeSlice 𝓕.c).symm (constantTime (diracDelta ℝ r₀))) ε) =
  0
    rw [oneDimPointParticle_div_electricFieldleft𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
      ((SpaceTime.distTimeSlice 𝓕.c).symm ((𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime (q • diracDelta ℝ r₀))) ε -
    𝓕.c.val * (q * ((SpaceTime.distTimeSlice 𝓕.c).symm (constantTime (diracDelta ℝ r₀))) ε) =
  0left𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
      ((SpaceTime.distTimeSlice 𝓕.c).symm ((𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime (q • diracDelta ℝ r₀))) ε -
    𝓕.c.val * (q * ((SpaceTime.distTimeSlice 𝓕.c).symm (constantTime (diracDelta ℝ r₀))) ε) =
  0]left𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
      ((SpaceTime.distTimeSlice 𝓕.c).symm ((𝓕.μ₀ * 𝓕.c.val ^ 2) • constantTime (q • diracDelta ℝ r₀))) ε -
    𝓕.c.val * (q * ((SpaceTime.distTimeSlice 𝓕.c).symm (constantTime (diracDelta ℝ r₀))) ε) =
  0
    simp only [map_smul, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]left𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
      (𝓕.μ₀ * 𝓕.c.val ^ 2 * (q * ((SpaceTime.distTimeSlice 𝓕.c).symm (constantTime (diracDelta ℝ r₀))) ε)) -
    𝓕.c.val * (q * ((SpaceTime.distTimeSlice 𝓕.c).symm (constantTime (diracDelta ℝ r₀))) ε) =
  0
    field_simpleft𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)⊢ 𝓕.c.val * q * ((SpaceTime.distTimeSlice 𝓕.c).symm (constantTime (diracDelta ℝ r₀))) ε * (1 - 1) = 0
    ringAll goals completed! 🐙
  ·right𝓕:FreeSpaceq:ℝr₀:Space 1⊢ ∀ (ε : 𝓢(SpaceTime 1, ℝ)) (i : Fin 1),
  (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inr i) = 0 intro ε iright𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)i:Fin 1⊢ (gradLagrangian 𝓕 (oneDimPointParticle 𝓕 q r₀) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)) ε (Sum.inr i) = 0
    rw [gradLagrangian_sum_inr_iright𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)i:Fin 1⊢ 𝓕.μ₀⁻¹ *
      (1 / 𝓕.c.val ^ 2 *
          (((SpaceTime.distTimeSlice 𝓕.c).symm (distTimeDeriv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀))))
                ε).ofLp
            i -
        ∑ j,
          (((PiLp.basisFun 2 ℝ (Fin 1)).tensorProduct (PiLp.basisFun 2 ℝ (Fin 1))).repr
              (((SpaceTime.distTimeSlice 𝓕.c).symm
                  ((distSpaceDeriv j) ((magneticFieldMatrix 𝓕.c) (oneDimPointParticle 𝓕 q r₀))))
                ε))
            (j, i)) +
    (((SpaceTime.distTimeSlice 𝓕.c).symm
            ((DistLorentzCurrentDensity.currentDensity 𝓕.c) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)))
          ε).ofLp
      i =
  0right𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)i:Fin 1⊢ 𝓕.μ₀⁻¹ *
      (1 / 𝓕.c.val ^ 2 *
          (((SpaceTime.distTimeSlice 𝓕.c).symm (distTimeDeriv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀))))
                ε).ofLp
            i -
        ∑ j,
          (((PiLp.basisFun 2 ℝ (Fin 1)).tensorProduct (PiLp.basisFun 2 ℝ (Fin 1))).repr
              (((SpaceTime.distTimeSlice 𝓕.c).symm
                  ((distSpaceDeriv j) ((magneticFieldMatrix 𝓕.c) (oneDimPointParticle 𝓕 q r₀))))
                ε))
            (j, i)) +
    (((SpaceTime.distTimeSlice 𝓕.c).symm
            ((DistLorentzCurrentDensity.currentDensity 𝓕.c) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)))
          ε).ofLp
      i =
  0]right𝓕:FreeSpaceq:ℝr₀:Space 1ε:𝓢(SpaceTime 1, ℝ)i:Fin 1⊢ 𝓕.μ₀⁻¹ *
      (1 / 𝓕.c.val ^ 2 *
          (((SpaceTime.distTimeSlice 𝓕.c).symm (distTimeDeriv ((electricField 𝓕.c) (oneDimPointParticle 𝓕 q r₀))))
                ε).ofLp
            i -
        ∑ j,
          (((PiLp.basisFun 2 ℝ (Fin 1)).tensorProduct (PiLp.basisFun 2 ℝ (Fin 1))).repr
              (((SpaceTime.distTimeSlice 𝓕.c).symm
                  ((distSpaceDeriv j) ((magneticFieldMatrix 𝓕.c) (oneDimPointParticle 𝓕 q r₀))))
                ε))
            (j, i)) +
    (((SpaceTime.distTimeSlice 𝓕.c).symm
            ((DistLorentzCurrentDensity.currentDensity 𝓕.c) (oneDimPointParticleCurrentDensity 𝓕.c q r₀)))
          ε).ofLp
      i =
  0
    simpAll goals completed! 🐙