Research proof index

The variational gradient of the free current potential for distributional potentials. -/ noncomputable def gradFreeCurrentPotential {d} : DistLorentzCurrentDensity d →ₗ[ℝ] ((SpaceTime d) →d[ℝ] Lorentz.Vector d) where toFun J := { toFun ε := ∑ μ, (η μ μ • (J ε μ) • Lorentz.Vector.basis μ) map_add' ε₁ ε₂ := by simp [Finset.sum_add_distrib, add_smul] map_smu...

The potential energy from the interaction of the electromagnetic potential with the free current J. -/ noncomputable def freeCurrentPotential (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) (x : SpaceTime d) : ℝ := ⟪A x, J x⟫ₘ /-! ### A.1. Shifts in the free current potential under shifts in the potential -/ lemma freeCurrentPotential_add...

The variational gradient of the lagrangian of electromagnetic field. -/ noncomputable def gradLagrangian {d} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : SpaceTime d → Lorentz.Vector d := (δ (q':=A), ∫ x, lagrangian 𝓕 ⟨q'⟩ J x) /-! ### C.3. The variational gradient in terms of the gradient of the kinetic term -/ lemma...

The Lagrangian is equal to 1/2 * (ε₀ E^2 - 1/μ₀ B^2) - φρ + A · j-/ lemma lagrangian_eq_electric_magnetic {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) (x : SpaceTime d) : A.lagrangian 𝓕 J x = 1 / 2 * (𝓕.ε₀ * ‖A.electricField 𝓕.c (x.time 𝓕.c) x.space‖ ^ 2 - (1 / (2 * 𝓕.μ₀)) * ∑ i, ∑ j, ‖A....