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.CurrentDensity
public import Physlib.Electromagnetism.Distributional.Dynamics.KineticTerm
public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProductThe Lagrangian in electromagnetism
i. Overview
In this module we define the Lagrangian density for the electromagnetic field in presence of a current density. We prove properties of this lagrangian density, and find it's variational gradient.
The lagrangian density is given by
L = -1/(4 μ₀) F_{μν} F^{μν} - A_μ J^μ
In this implementation we set μ₀ = 1. It is a TODO to introduce this constant.
ii. Key results
gradFreeCurrentPotential : The variational gradient of the free current potential.
gradLagrangian : The variational gradient of the lagrangian density.
iii. Table of contents
A. The gradient of the lagrangian density for distributions
A.1. The gradient of the free current potential
A.1.1. Free current potential as a tensor
A.2. The gradient of the lagrangian density
A.2.1. The lagrangian gradient as a tensor
iv. References
https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf
@[expose] public sectionA. The gradient of the lagrangian density for distributions
attribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_oneA.1. The gradient of the free current potential
We define this through the lemma gradFreeCurrentPotential_eq_sum_basis
lemma gradFreeCurrentPotential_eq_sum_basis {d}
(J : DistLorentzCurrentDensity d) (ε : 𝓢(SpaceTime d, ℝ)) :
(gradFreeCurrentPotential J) ε =
(∑ μ, (η μ μ • (J ε μ) • Lorentz.Vector.basis μ)) := rfl𝓕:FreeSpaced:ℕJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)⊢ J ε (Sum.inl 0) = ((distTimeSlice 𝓕.c).symm ((distTimeSlice 𝓕.c) J)) ε (Sum.inl 0)
All goals completed! 🐙𝓕:FreeSpaced:ℕJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)i:Fin d⊢ -1 * J ε (Sum.inr i) = -((distTimeSlice 𝓕.c).symm ((distTimeSlice 𝓕.c) J)) ε (Sum.inr i)
All goals completed! 🐙A.1.1. Free current potential as a tensor
d:ℕJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ (∑ μ, η μ μ • J ε μ • Lorentz.Vector.basis μ) ν = η ν ν * J ε ν
All goals completed! 🐙D.2. The gradient of the lagrangian density
Defined through gradLagrangian_eq_kineticTerm_sub.
lemma gradLagrangian_sum_inl_0 {𝓕 : FreeSpace}
(A : DistElectromagneticPotential d) (J : DistLorentzCurrentDensity d)
(ε : 𝓢(SpaceTime d, ℝ)) :
A.gradLagrangian 𝓕 J ε (Sum.inl 0) =
(1/(𝓕.μ₀ * 𝓕.c) * (distTimeSlice 𝓕.c).symm (Space.distSpaceDiv (A.electricField 𝓕.c)) ε)
- 𝓕.c * (distTimeSlice 𝓕.c).symm (J.chargeDensity 𝓕.c) ε := d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)⊢ (gradLagrangian 𝓕 A J) ε (Sum.inl 0) =
1 / (𝓕.μ₀ * 𝓕.c.val) * ((distTimeSlice 𝓕.c).symm (Space.distSpaceDiv ((electricField 𝓕.c) A))) ε -
𝓕.c.val * ((distTimeSlice 𝓕.c).symm ((DistLorentzCurrentDensity.chargeDensity 𝓕.c) J)) ε
All goals completed! 🐙lemma gradLagrangian_sum_inr_i {𝓕 : FreeSpace}
(A : DistElectromagneticPotential d) (J : DistLorentzCurrentDensity d)
(ε : 𝓢(SpaceTime d, ℝ)) (i : Fin d) :
A.gradLagrangian 𝓕 J ε (Sum.inr i) =
𝓕.μ₀⁻¹ * (1 / 𝓕.c ^ 2 *
(distTimeSlice 𝓕.c).symm (Space.distTimeDeriv (A.electricField 𝓕.c)) ε i -
∑ j, ((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
((distTimeSlice 𝓕.c).symm (Space.distSpaceDeriv j (A.magneticFieldMatrix 𝓕.c)) ε) (j, i)) +
(distTimeSlice 𝓕.c).symm (J.currentDensity 𝓕.c) ε i := d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)i:Fin d⊢ (gradLagrangian 𝓕 A J) ε (Sum.inr i) =
𝓕.μ₀⁻¹ *
(1 / 𝓕.c.val ^ 2 * (((distTimeSlice 𝓕.c).symm (Space.distTimeDeriv ((electricField 𝓕.c) A))) ε).ofLp i -
∑ j,
(((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr
(((distTimeSlice 𝓕.c).symm ((Space.distSpaceDeriv j) ((magneticFieldMatrix 𝓕.c) A))) ε))
(j, i)) +
(((distTimeSlice 𝓕.c).symm ((DistLorentzCurrentDensity.currentDensity 𝓕.c) J)) ε).ofLp i
All goals completed! 🐙A.2.1. The lagrangian gradient as a tensor
d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ J ε ν = Tensorial.toTensor.symm (Tensorial.toTensor (J ε)) νd:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ![0] = id
d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ![0] = id
d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin di:Fin (Nat.succ 0)⊢ ![0] i = id i
d:ℕ𝓕:FreeSpaceA:DistElectromagneticPotential dJ:DistLorentzCurrentDensity dε:𝓢(SpaceTime d, ℝ)ν:Fin 1 ⊕ Fin d⊢ ![0] ((fun i => i) ⟨0, ⋯⟩) = id ((fun i => i) ⟨0, ⋯⟩)
All goals completed! 🐙