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 prover properties of this lagrangian density, and find it's variational gradient.

ii. Key results

• 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. The Lagrangian density
  • A.1. Shifts in the lagrangian under shifts in the potential
• B. The variational gradient of the lagrangian density
  • B.1. The lagrangian density has a variational gradient
  • B.2. The definition of, gradLagrangian, the variational gradient of the lagrangian density
  • B.3. The variational gradient in terms of the gradient of the kinetic term
  • B.4. The lagrangian density has the variational gradient equal to gradLagrangian
  • B.5. The variational gradient in terms of the field strength tensor
  • B.6. The lagrangian gradient recovering Gauss's and Ampère laws

iv. References

• https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html

A. 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 : ℕ} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) (x : SpaceTime d) : ℝ

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

Equations

• A.lagrangian J x = A.kineticTerm x - (Lorentz.Vector.minkowskiProduct (A x)) (J x)

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

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

B. The variational gradient of the lagrangian density

B.1. The lagrangian density has a variational gradient

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

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

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

The variational gradient of the lagrangian of electromagnetic field.

Equations

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

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

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

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

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

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

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

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

theorem Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_electricField_magneticField (A : ElectromagneticPotential) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity) (hJ : ContDiff ℝ (↑⊤) J) (x : SpaceTime) : A.gradLagrangian J x = (Space.div (A.electricField (SpaceTime.time x)) (SpaceTime.space x) - J.chargeDensity (SpaceTime.time x) (SpaceTime.space x)) • Lorentz.Vector.basis (Sum.inl 0) + ∑ i : Fin 3, (Time.deriv (fun (x_1 : Time) => A.electricField x_1 (SpaceTime.space x)) (SpaceTime.time x) - Space.curl (A.magneticField (SpaceTime.time x)) (SpaceTime.space x) + J.currentDensity (SpaceTime.time x) (SpaceTime.space x)) i • Lorentz.Vector.basis (Sum.inr i)