The 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

• freeCurrentPotential : The potential energy from the interaction of the electromagnetic potential with a free Lorentz current density.
• gradFreeCurrentPotential : The variational gradient of the free current potential.
• lagrangian : The lagrangian density for the electromagnetic field in presence of a Lorentz current density.
• gradLagrangian : The variational gradient of the lagrangian density.
• gradLagrangian_eq_electricField_magneticField : The variational gradient of the lagrangian density expressed in Gauss's and Ampère laws.

iii. Table of contents

• A. Free current potential
  • A.1. Shifts in the free current potential under shifts in the potential
  • A.2. The free current potential has a variational gradient
  • A.3. The free current potential in terms of the scalar and vector potentials
  • A.4. The variational gradient of the free current potential
• B. The Lagrangian density
  • B.1. Shifts in the lagrangian under shifts in the potential
  • B.2. Lagrangian in terms of electric and magnetic fields
• C. The variational gradient of the lagrangian density
  • C.1. The lagrangian density has a variational gradient
  • C.2. The definition of, gradLagrangian, the variational gradient of the lagrangian density
  • C.3. The variational gradient in terms of the gradient of the kinetic term
  • C.4. The lagrangian density has the variational gradient equal to gradLagrangian
  • C.5. The variational gradient in terms of the field strength tensor
  • C.6. The lagrangian gradient recovering Gauss's and Ampère laws

iv. References

• https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
• https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf

A. Free current potential

noncomputable def Electromagnetism.ElectromagneticPotential.freeCurrentPotential {d : ℕ} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) (x : SpaceTime d) : ℝ

The potential energy from the interaction of the electromagnetic potential with the free current J.

Equations

• A.freeCurrentPotential J x = (Lorentz.Vector.minkowskiProduct (A x)) (J x)

A.1. Shifts in the free current potential under shifts in the potential

theorem Electromagnetism.ElectromagneticPotential.freeCurrentPotential_add_const {d : ℕ} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) (c : Lorentz.Vector d) (x : SpaceTime d) : freeCurrentPotential (fun (x : SpaceTime d) => A x + c) J x = A.freeCurrentPotential J x + (Lorentz.Vector.minkowskiProduct c) (J x)

A.2. The free current potential has a variational gradient

theorem Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt {d : ℕ} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) : HasVarGradientAt (fun (A : SpaceTime d → Lorentz.Vector d) => freeCurrentPotential A J) (∑ μ : Fin 1 ⊕ Fin d, fun (x : SpaceTime d) => (minkowskiMatrix μ μ * J x μ) • Lorentz.Vector.basis μ) A

A.3. The free current potential in terms of the scalar and vector potentials

theorem Electromagnetism.ElectromagneticPotential.freeCurrentPotential_eq_sum_scalarPotential_vectorPotential {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) (x : SpaceTime d) : A.freeCurrentPotential J x = scalarPotential 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) - ∑ i : Fin d, vectorPotential 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i * LorentzCurrentDensity.currentDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i

A.4. The variational gradient of the free current potential

noncomputable def Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential {d : ℕ} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : SpaceTime d → Lorentz.Vector d

The variational gradient of the free current potential.

Equations

• A.gradFreeCurrentPotential J = varGradient (fun (q' : SpaceTime d → Lorentz.Vector d) (x : SpaceTime d) => Electromagnetism.ElectromagneticPotential.freeCurrentPotential q' J x) A

theorem Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis {d : ℕ} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) : A.gradFreeCurrentPotential J = ∑ μ : Fin 1 ⊕ Fin d, fun (x : SpaceTime d) => (minkowskiMatrix μ μ * J x μ) • Lorentz.Vector.basis μ

theorem Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_chargeDensity_currentDensity {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) (x : SpaceTime d) : A.gradFreeCurrentPotential J x = (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)) • Lorentz.Vector.basis (Sum.inl 0) + ∑ i : Fin d, -LorentzCurrentDensity.currentDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i • Lorentz.Vector.basis (Sum.inr i)

B. The Lagrangian density

The lagrangian density for the electromagnetic field in presence of a current density J is L = -1/(4 μ₀) F_{μν} F^{μν} - A_μ J^μ

noncomputable def Electromagnetism.ElectromagneticPotential.lagrangian {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) (x : SpaceTime d) : ℝ

The lagrangian density associated with a electromagnetic potential and a Lorentz current density.

Equations

• Electromagnetism.ElectromagneticPotential.lagrangian 𝓕 A J x = Electromagnetism.ElectromagneticPotential.kineticTerm 𝓕 A x - A.freeCurrentPotential J x

B.1. Shifts in the lagrangian under shifts in the potential

theorem Electromagnetism.ElectromagneticPotential.lagrangian_add_const {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) (c : Lorentz.Vector d) (x : SpaceTime d) : lagrangian 𝓕 (fun (x : SpaceTime d) => A x + c) J x = lagrangian 𝓕 A J x - (Lorentz.Vector.minkowskiProduct c) (J x)

B.2. Lagrangian in terms of electric and magnetic fields

theorem Electromagnetism.ElectromagneticPotential.lagrangian_eq_electric_magnetic {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) (x : SpaceTime d) : lagrangian 𝓕 A J x = 1 / 2 * (𝓕.ε₀ * ‖electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)‖ ^ 2 - 1 / (2 * 𝓕.μ₀) * ∑ i : Fin d, ∑ j : Fin d, ‖magneticFieldMatrix 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) (i, j)‖ ^ 2) - scalarPotential 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) + ∑ i : Fin d, vectorPotential 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i * LorentzCurrentDensity.currentDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i

The Lagrangian is equal to 1/2 * (ε₀ E^2 - 1/μ₀ B^2) - φρ + A · j

C. The variational gradient of the lagrangian density

C.1. The lagrangian density has a variational gradient

theorem Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_eq_add_gradKineticTerm {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) : HasVarGradientAt (fun (A : SpaceTime d → Lorentz.Vector d) => lagrangian 𝓕 A J) (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) A

C.2. The definition of, gradLagrangian, the variational gradient of the lagrangian density

noncomputable def Electromagnetism.ElectromagneticPotential.gradLagrangian {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : SpaceTime d → Lorentz.Vector d

The variational gradient of the lagrangian of electromagnetic field.

Equations

• One or more equations did not get rendered due to their size.

C.3. The variational gradient in terms of the gradient of the kinetic term

theorem Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_kineticTerm_sub {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) : gradLagrangian 𝓕 A J = gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J

C.4. The lagrangian density has the variational gradient equal to gradLagrangian

theorem Electromagnetism.ElectromagneticPotential.lagrangian_hasVarGradientAt_gradLagrangian {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) : HasVarGradientAt (fun (A : SpaceTime d → Lorentz.Vector d) => lagrangian 𝓕 A J) (gradLagrangian 𝓕 A J) A

C.5. The variational gradient in terms of the field strength tensor

theorem Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_sum_fieldStrengthMatrix {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) : gradLagrangian 𝓕 A J = fun (x : SpaceTime d) => ∑ ν : Fin 1 ⊕ Fin d, minkowskiMatrix ν ν • (1 / 𝓕.μ₀ * ∑ μ : Fin 1 ⊕ Fin d, SpaceTime.deriv μ (fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis ν

C.6. The lagrangian gradient recovering Gauss's and Ampère laws

theorem Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) (x : SpaceTime d) : gradLagrangian 𝓕 A J x = (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x)) (SpaceTime.space x) + -𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)) • Lorentz.Vector.basis (Sum.inl 0) + ∑ i : Fin d, (𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * Time.deriv (fun (x_1 : Time) => electricField 𝓕.c A x_1 (SpaceTime.space x)) ((SpaceTime.time 𝓕.c) x) i - ∑ j : Fin d, Space.deriv j (fun (x_1 : Space d) => magneticFieldMatrix 𝓕.c A ((SpaceTime.time 𝓕.c) x) x_1 (j, i)) (SpaceTime.space x)) + LorentzCurrentDensity.currentDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i) • Lorentz.Vector.basis (Sum.inr i)