Extrema of the Lagrangian density

i. Overview

In this module we define what it means for an electromagnetic potential to be an extremum of the Lagrangian density in presence of a Lorentz current density.

This is equivalent to the electromagnetic potential satisfying Maxwell's equations with sources, i.e. Gauss's law and Ampère's law.

ii. Key results

• IsExtrema : The condition on an electromagnetic potential to be an extrema of the lagrangian.
• isExtrema_iff_gauss_ampere_magneticFieldMatrix : The electromagnetic potential is an extrema of the lagrangian if and only if Gauss's law and Ampère's law hold (in terms of the magnetic field matrix).
• time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema : A wave-like equation for the magnetic field matrix from the extrema condition.
• time_deriv_time_deriv_electricField_of_isExtrema : A wave-like equation for the electric field from the extrema condition.

iii. Table of contents

• A. The condition for an extrema of the Lagrangian density
  • A.1. Extrema condition in terms of the field strength matrix
• B. Gauss's law and Ampère's law and the extrema condition
• C. Time derivatives from the extrema condition
• D. Second time derivatives from the extrema condition
  • D.1. Second time derivatives of the magnetic field from the extrema condition
  • D.2. Second time derivatives of the electric field from the extrema condition

iv. References

A. The condition for an extrema of the Lagrangian density

def Electromagnetism.ElectromagneticPotential.IsExtrema {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : Prop

The condition on an electromagnetic potential to be an extrema of the lagrangian.

Equations

• Electromagnetism.ElectromagneticPotential.IsExtrema 𝓕 A J = (Electromagnetism.ElectromagneticPotential.gradLagrangian 𝓕 A J = 0)

theorem Electromagnetism.ElectromagneticPotential.isExtrema_iff_gradLagrangian {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : IsExtrema 𝓕 A J ↔ gradLagrangian 𝓕 A J = 0

A.1. Extrema condition in terms of the field strength matrix

theorem Electromagnetism.ElectromagneticPotential.isExtrema_iff_fieldStrengthMatrix {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) : IsExtrema 𝓕 A J ↔ ∀ (x : SpaceTime d) (ν : Fin 1 ⊕ Fin d), ∑ μ : Fin 1 ⊕ Fin d, SpaceTime.deriv μ (fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀ * J x ν

B. Gauss's law and Ampère's law and the extrema condition

theorem Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix {d : ℕ} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) : IsExtrema 𝓕 A J ↔ ∀ (t : Time) (x : Space d), Space.div (electricField 𝓕.c A t) x = LorentzCurrentDensity.chargeDensity 𝓕.c J t x / 𝓕.ε₀ ∧ ∀ (i : Fin d), 𝓕.μ₀ * 𝓕.ε₀ * Time.deriv (fun (t : Time) => electricField 𝓕.c A t x) t i = ∑ j : Fin d, Space.deriv j (fun (x : Space d) => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 𝓕.μ₀ * LorentzCurrentDensity.currentDensity 𝓕.c J t x i

C. Time derivatives from the extrema condition

theorem Electromagnetism.ElectromagneticPotential.time_deriv_electricField_of_isExtrema {d : ℕ} {A : ElectromagneticPotential d} {𝓕 : FreeSpace} (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) (h : IsExtrema 𝓕 A J) (t : Time) (x : Space d) (i : Fin d) : Time.deriv (fun (x_1 : Time) => electricField 𝓕.c A x_1 x) t i = 1 / (𝓕.μ₀ * 𝓕.ε₀) * ∑ j : Fin d, Space.deriv j (fun (x : Space d) => magneticFieldMatrix 𝓕.c A t x (j, i)) x - 1 / 𝓕.ε₀ * LorentzCurrentDensity.currentDensity 𝓕.c J t x i

D. Second time derivatives from the extrema condition

D.1. Second time derivatives of the magnetic field from the extrema condition

theorem Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema {d : ℕ} {A : ElectromagneticPotential d} {𝓕 : FreeSpace} (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJd : Differentiable ℝ J) (hJ : ContDiff ℝ (↑⊤) J) (h : IsExtrema 𝓕 A J) (t : Time) (x : Space d) (i j : Fin d) : Time.deriv (Time.deriv fun (x_1 : Time) => magneticFieldMatrix 𝓕.c A x_1 x (i, j)) t = 𝓕.c.val ^ 2 * ∑ k : Fin d, Space.deriv k (Space.deriv k fun (x : Space d) => magneticFieldMatrix 𝓕.c A t x (i, j)) x + 𝓕.ε₀⁻¹ * (Space.deriv j (fun (x : Space d) => LorentzCurrentDensity.currentDensity 𝓕.c J t x i) x - Space.deriv i (fun (x : Space d) => LorentzCurrentDensity.currentDensity 𝓕.c J t x j) x)

D.2. Second time derivatives of the electric field from the extrema condition

theorem Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema {d : ℕ} {A : ElectromagneticPotential d} {𝓕 : FreeSpace} (hA : ContDiff ℝ (↑⊤) A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ (↑⊤) J) (h : IsExtrema 𝓕 A J) (t : Time) (x : Space d) (i : Fin d) : Time.deriv (Time.deriv fun (x_1 : Time) => electricField 𝓕.c A x_1 x i) t = 𝓕.c.val ^ 2 * ∑ j : Fin d, Space.deriv j (Space.deriv j fun (x : Space d) => electricField 𝓕.c A t x i) x - 𝓕.c.val ^ 2 / 𝓕.ε₀ * Space.deriv i (fun (x : Space d) => LorentzCurrentDensity.chargeDensity 𝓕.c J t x) x - 𝓕.c.val ^ 2 * 𝓕.μ₀ * Time.deriv (fun (x_1 : Time) => LorentzCurrentDensity.currentDensity 𝓕.c J x_1 x i) t