PhysLean Documentation

PhysLean.Electromagnetism.Dynamics.IsExtrema

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 #

iii. Table of contents #

iv. References #

A. The condition for an extrema of the Lagrangian density #

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

Equations
Instances For

    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 ν

    A.2. Extrema condition in terms of tensors #

    The electromagnetic potential is an exterma of the lagrangian if and only if

    $$\frac{1}{\mu_0} \partial_\mu F^{\mu \nu} - J^{\nu} = 0.$$

    A.3. Equivariance of the extrema condition #

    If A is an extrema of the lagrangian with current density J, then the Lorentz transformation Λ • A (Λ⁻¹ • x) is an extrema of the lagrangian with current density Λ • J (Λ⁻¹ • x).

    Combined with time_deriv_time_deriv_electricField_of_isExtrema, this shows that the speed with which an electromagnetic wave propagates is invariant under Lorentz transformations.

    theorem Electromagnetism.ElectromagneticPotential.isExtrema_lorentzGroup_apply_iff {d : } {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff (↑) A) (J : LorentzCurrentDensity d) (hJ : ContDiff (↑) J) (Λ : (LorentzGroup d)) :
    (IsExtrema 𝓕 (fun (x : SpaceTime d) => Λ A (Λ⁻¹ x)) fun (x : SpaceTime d) => Λ J (Λ⁻¹ x)) IsExtrema 𝓕 A J

    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).ofLp 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).ofLp 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).ofLp 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).ofLp i

    D. Second time derivatives from the extrema condition #

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

    We show that the magnetic field matrix $B_{ij}$ satisfies the following wave-like equation

    $$\frac{\partial^2 B_{ij}}{\partial t^2} = c^2 \sum_k \frac{\partial^2 B_{ij}}{\partial x_k^2}

    When the free current density is zero, this reduces to the wave equation.

    theorem Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_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 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).ofLp i) x - Space.deriv i (fun (x : Space d) => (LorentzCurrentDensity.currentDensity 𝓕.c J t x).ofLp j) x)

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

    We show that the electric field $E_i$ satisfies the following wave-like equation:

    $$\frac{\partial^2 E_{i}}{\partial t^2} = c^2 \sum_k \frac{\partial^2 E_{i}}{\partial x_k^2}

    When the free current density and charge density are zero, this reduces to the wave equation.

    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).ofLp i) t = 𝓕.c.val ^ 2 * j : Fin d, Space.deriv j (Space.deriv j fun (x : Space d) => (electricField 𝓕.c A t x).ofLp 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).ofLp i) t

    E. Is Extema condition in the distributional case #

    The above results looked at the extrema condition for electromagnetic potentials that are functions. We now look at the case where the electromagnetic potential is a distribution.

    The proposition on an electromagnetic potential, corresponding to the statement that it is an extrema of the lagrangian.

    Equations
    Instances For

      E.1. IsExtrema and Gauss's law and Ampère's law #

      We show that A is an extrema of the lagrangian if and only if Gauss's law and Ampère's law hold. In other words,

      $$\nabla \cdot \mathbf{E} = \frac{\rho}{\varepsilon_0}$$ and $$\mu_0 \varepsilon_0 \frac{\partial \mathbf{E}_i}{\partial t} - ∑ j, \partial_j \mathbf{B}_{j i} + \mu_0 \mathbf{J}_i = 0.$$ Here $\mathbf{B}$ is the magnetic field matrix.

      E.2. IsExtrema in terms of Vector Potentials #

      We show that A is an extrema of the lagrangian if and only if Gauss's law and Ampère's law hold. In other words,

      $$\nabla \cdot \mathbf{E} = \frac{\rho}{\varepsilon_0}$$ and $$\mu_0 \varepsilon_0 \frac{\partial \mathbf{E}_i}{\partial t} - ∑ j, -(\partial_j \partial_j \vec A_i - \partial_j \partial_i \vec A_j)

      E.3. The exterma condition in terms of tensors #

      We show that A is an extrema of the lagrangian if and only if the equation $$(\frac{1}{\mu_0} \partial_\kappa F^{\kappa \nu'} - J^{\nu'}) = 0,$$ holds.

      E.4. The invariance of the exterma condition under Lorentz transformations #

      We show that the Exterma condition is invariant under Lorentz transformations. This implies that if an electromagnetic potential is an extrema in one inertial frame, it is also an extrema in any other inertial frame. In otherwords that the Maxwell's equations are Lorentz invariant. A natural consequence of this is that the speed of light is the same in all inertial frames.