Physlib.Electromagnetism.Dynamics.Lagrangian

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.Dynamics.CurrentDensity
public import Physlib.Electromagnetism.Dynamics.KineticTerm
public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct

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

C.7. The lagrangian gradient in tensor notation

iv. References

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

https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf

              @[expose] public sectionattribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_one

A. Free current potential

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

lemma freeCurrentPotential_add_const (A : ElectromagneticPotential d)
    (J : LorentzCurrentDensity d) (c : Lorentz.Vector d) (x : SpaceTime d) :
    freeCurrentPotential ⟨fun x => A x + c⟩ J x = freeCurrentPotential A J x + ⟪c, J x⟫ₘ := byd:ℕA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ { val := fun x => A.val x + c }.freeCurrentPotential J x = A.freeCurrentPotential J x + (minkowskiProduct c) (J x)
  simp [freeCurrentPotential]All goals completed! 🐙

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



lemma freeCurrentPotential_hasVarGradientAt (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d)
    (hJ : ContDiff ℝ ∞ J) :
    HasVarGradientAt (fun A => freeCurrentPotential ⟨A⟩ J)
    (((∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ))) A := byd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun A => { val := A }.freeCurrentPotential J) (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
  conv =>d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J| HasVarGradientAt (fun A => { val := A }.freeCurrentPotential J) (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
    enter [1, q', x]d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jq':SpaceTime d → Lorentz.Vector dx:SpaceTime d| { val := q' }.freeCurrentPotential J x
    rw [freeCurrentPotential, minkowskiProduct_toCoord_minkowskiMatrix]d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jq':SpaceTime d → Lorentz.Vector dx:SpaceTime d| ∑ μ, η μ μ * { val := q' }.val x μ * J x μ
  apply HasVarGradientAt.sum _ hAd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ ∀ (i : Fin 1 ⊕ Fin d),
  HasVarGradientAt (fun v x => η i i * { val := v }.val x i * J x i) (fun x => (η i i * J x i) • Lorentz.Vector.basis i)
    A.val
  intro μd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin d⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
  have h1 := hasVarAdjDerivAt_component μ A hAd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.val⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
  have h2' : ContDiff ℝ ∞ fun x => η μ μ * J x μ :=
    ContDiff.mul (byd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.val⊢ ContDiff ℝ ∞ fun x => η μ μd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val fun_propAll goals completed! 🐙d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val) ((Lorentz.Vector.contDiff_apply _).mpr hJ μ)d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
  have h2 := HasVarAdjDerivAt.fun_mul h2' _ _ A h1d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * J x μ * φ x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.val⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
  have h3' : (fun (φ : SpaceTime d → Lorentz.Vector d) x => η μ μ * J x μ * φ x μ) =
    (fun (φ : SpaceTime d → Lorentz.Vector d) x => η μ μ * φ x μ * J x μ) := byd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun A => { val := A }.freeCurrentPotential J) (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.vald:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * J x μ * φ x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valh3':(fun φ x => η μ μ * J x μ * φ x μ) = fun φ x => η μ μ * φ x μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
    funext φ xd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * J x μ * φ x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valφ:SpaceTime d → Lorentz.Vector dx:SpaceTime d⊢ η μ μ * J x μ * φ x μ = η μ μ * φ x μ * J x μd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * J x μ * φ x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valh3':(fun φ x => η μ μ * J x μ * φ x μ) = fun φ x => η μ μ * φ x μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
    ringd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * J x μ * φ x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valh3':(fun φ x => η μ μ * J x μ * φ x μ) = fun φ x => η μ μ * φ x μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.vald:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * J x μ * φ x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valh3':(fun φ x => η μ μ * J x μ * φ x μ) = fun φ x => η μ μ * φ x μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
  rw [h3'd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * φ x μ * J x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valh3':(fun φ x => η μ μ * J x μ * φ x μ) = fun φ x => η μ μ * φ x μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.vald:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * φ x μ * J x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valh3':(fun φ x => η μ μ * J x μ * φ x μ) = fun φ x => η μ μ * φ x μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val] at h2d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * φ x μ * J x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valh3':(fun φ x => η μ μ * J x μ * φ x μ) = fun φ x => η μ μ * φ x μ * J x μ⊢ HasVarGradientAt (fun v x => η μ μ * { val := v }.val x μ * J x μ) (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ)
  A.val
  apply HasVarGradientAt.intro _ h2d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jμ:Fin 1 ⊕ Fin dh1:HasVarAdjDerivAt (fun A' x => A' x μ) (fun A' x => A' x • Lorentz.Vector.basis μ) A.valh2':ContDiff ℝ ∞ fun x => η μ μ * J x μh2:HasVarAdjDerivAt (fun φ x => η μ μ * φ x μ * J x μ)
  (fun ψ x => (fun x' => η μ μ * J x' μ * ψ x') x • Lorentz.Vector.basis μ) A.valh3':(fun φ x => η μ μ * J x μ * φ x μ) = fun φ x => η μ μ * φ x μ * J x μ⊢ (fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) = fun x =>
  (fun x' => η μ μ * J x' μ * (fun x => 1) x') x • Lorentz.Vector.basis μ
  simpAll goals completed! 🐙

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



lemma freeCurrentPotential_eq_sum_scalarPotential_vectorPotential
    (𝓕 : FreeSpace) (A : ElectromagneticPotential d)
    (J : LorentzCurrentDensity d) (x : SpaceTime d) :
    A.freeCurrentPotential J x =
    A.scalarPotential 𝓕.c (x.time 𝓕.c) x.space * J.chargeDensity 𝓕.c (x.time 𝓕.c) x.space
    - ∑ i, A.vectorPotential 𝓕.c (x.time 𝓕.c) x.space i *
        J.currentDensity 𝓕.c (x.time 𝓕.c) x.space i := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dx:SpaceTime d⊢ A.freeCurrentPotential J x =
  scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i
  rw [freeCurrentPotential,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dx:SpaceTime d⊢ (minkowskiProduct (A.val x)) (J x) =
  scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp id:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ μ, η μ μ * A.val x μ * J x μ =
  scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i minkowskiProduct_toCoord_minkowskiMatrixd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ μ, η μ μ * A.val x μ * J x μ =
  scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp id:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ μ, η μ μ * A.val x μ * J x μ =
  scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ μ, η μ μ * A.val x μ * J x μ =
  scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i
  simp [Fintype.sum_sum_type, scalarPotential, vectorPotential, LorentzCurrentDensity.chargeDensity,
    LorentzCurrentDensity.currentDensity, timeSlice]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dx:SpaceTime d⊢ A.val x (Sum.inl 0) * J x (Sum.inl 0) + -∑ x_1, A.val x (Sum.inr x_1) * J x (Sum.inr x_1) =
  𝓕.c.val * A.val x (Sum.inl 0) * (𝓕.c.val⁻¹ * J x (Sum.inl 0)) - ∑ x_1, A.val x (Sum.inr x_1) * J x (Sum.inr x_1)
  field_simpd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dx:SpaceTime d⊢ A.val x (Sum.inl 0) * J x (Sum.inl 0) + -∑ x_1, A.val x (Sum.inr x_1) * J x (Sum.inr x_1) =
  A.val x (Sum.inl 0) * J x (Sum.inl 0) - ∑ x_1, A.val x (Sum.inr x_1) * J x (Sum.inr x_1)
  ringAll goals completed! 🐙

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

              lemma gradFreeCurrentPotential_eq_sum_basis {d} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d)
    (hJ : ContDiff ℝ ∞ J) :
    A.gradFreeCurrentPotential J = (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) := byd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ A.gradFreeCurrentPotential J = ∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ
  exact (freeCurrentPotential_hasVarGradientAt A hA J hJ).varGradientAll goals completed! 🐙

lemma 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 * J.chargeDensity 𝓕.c (x.time 𝓕.c) x.space) • Lorentz.Vector.basis (Sum.inl 0) +
      (∑ i, - J.currentDensity 𝓕.c (x.time 𝓕.c) x.space i • Lorentz.Vector.basis (Sum.inr i)) := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ A.gradFreeCurrentPotential J x =
  (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      -(LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)
  rw [gradFreeCurrentPotential_eq_sum_basis A hA J hJd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x =
  (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      -(LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x =
  (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      -(LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x =
  (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      -(LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)
  rw [Fintype.sum_sum_typed:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ((∑ a₁, fun x => (η (Sum.inl a₁) (Sum.inl a₁) * J x (Sum.inl a₁)) • Lorentz.Vector.basis (Sum.inl a₁)) +
      ∑ a₂, fun x => (η (Sum.inr a₂) (Sum.inr a₂) * J x (Sum.inr a₂)) • Lorentz.Vector.basis (Sum.inr a₂))
    x =
  (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      -(LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ((∑ a₁, fun x => (η (Sum.inl a₁) (Sum.inl a₁) * J x (Sum.inl a₁)) • Lorentz.Vector.basis (Sum.inl a₁)) +
      ∑ a₂, fun x => (η (Sum.inr a₂) (Sum.inr a₂) * J x (Sum.inr a₂)) • Lorentz.Vector.basis (Sum.inr a₂))
    x =
  (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      -(LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ((∑ a₁, fun x => (η (Sum.inl a₁) (Sum.inl a₁) * J x (Sum.inl a₁)) • Lorentz.Vector.basis (Sum.inl a₁)) +
      ∑ a₂, fun x => (η (Sum.inr a₂) (Sum.inr a₂) * J x (Sum.inr a₂)) • Lorentz.Vector.basis (Sum.inr a₂))
    x =
  (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      -(LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)
  simp only [Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton,
    inl_0_inl_0, one_mul, inr_i_inr_i, neg_mul, _root_.neg_smul, Pi.add_apply, Finset.sum_apply]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ J x (Sum.inl 0) • Lorentz.Vector.basis (Sum.inl 0) + ∑ c, -(J x (Sum.inr c) • Lorentz.Vector.basis (Sum.inr c)) =
  (𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      -((LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 •
          Lorentz.Vector.basis (Sum.inr x_1))
  congre_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ J x (Sum.inl 0) = 𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)e_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (fun c => -(J x (Sum.inr c) • Lorentz.Vector.basis (Sum.inr c))) = fun x_1 =>
  -((LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) <;>e_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ J x (Sum.inl 0) = 𝓕.c.val * LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)e_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (fun c => -(J x (Sum.inr c) • Lorentz.Vector.basis (Sum.inr c))) = fun x_1 =>
  -((LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1))
    simp [LorentzCurrentDensity.chargeDensity, LorentzCurrentDensity.currentDensity]All goals completed! 🐙

lemma gradFreeCurrentPotential_eq_tensor {d} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d)
    (hJ : ContDiff ℝ ∞ J) (x : SpaceTime d) (ν : Fin 1 ⊕ Fin d) :
    A.gradFreeCurrentPotential J x ν = η ν ν * ((Tensorial.toTensor (M := Lorentz.Vector d)).symm
    (permT id (IsReindexing.auto) {J x | ν'}ᵀ)) ν := byd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ A.gradFreeCurrentPotential J x ν = η ν ν * Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))) ν
  trans η ν ν * (Lorentz.Vector.basis.repr ((Tensorial.toTensor (M := Lorentz.Vector d)).symm
    (permT id (IsReindexing.auto) {J x | ν'}ᵀ))) νd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ A.gradFreeCurrentPotential J x ν =
  η ν ν * (Lorentz.Vector.basis.repr (Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))))) νd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν * (Lorentz.Vector.basis.repr (Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))))) ν =
  η ν ν * Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))) ν
  swapd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν * (Lorentz.Vector.basis.repr (Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))))) ν =
  η ν ν * Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))) νd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ A.gradFreeCurrentPotential J x ν =
  η ν ν * (Lorentz.Vector.basis.repr (Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))))) ν
  ·d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν * (Lorentz.Vector.basis.repr (Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))))) ν =
  η ν ν * Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))) ν simp [Lorentz.Vector.basis_repr_apply]All goals completed! 🐙
  simp [Lorentz.Vector.basis_repr_apply]d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ A.gradFreeCurrentPotential J x ν = η ν ν * J x ν
  rw [gradFreeCurrentPotential_eq_sum_basis A hA J hJd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x ν = η ν ν * J x νd:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x ν = η ν ν * J x ν]d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x ν = η ν ν * J x ν
  simp [Lorentz.Vector.apply_sum]All goals completed! 🐙

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^μ

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



lemma lagrangian_add_const {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
    (J : LorentzCurrentDensity d) (c : Lorentz.Vector d) (x : SpaceTime d) :
    lagrangian 𝓕 ⟨fun x => A x + c⟩ J x = lagrangian 𝓕 A J x - ⟪c, J x⟫ₘ := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ lagrangian 𝓕 { val := fun x => A.val x + c } J x = lagrangian 𝓕 A J x - (minkowskiProduct c) (J x)
  rw [lagrangian,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 { val := fun x => A.val x + c } x - { val := fun x => A.val x + c }.freeCurrentPotential J x =
  lagrangian 𝓕 A J x - (minkowskiProduct c) (J x)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 A x - (A.freeCurrentPotential J x + (minkowskiProduct c) (J x)) =
  kineticTerm 𝓕 A x - A.freeCurrentPotential J x - (minkowskiProduct c) (J x) lagrangian,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 { val := fun x => A.val x + c } x - { val := fun x => A.val x + c }.freeCurrentPotential J x =
  kineticTerm 𝓕 A x - A.freeCurrentPotential J x - (minkowskiProduct c) (J x)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 A x - (A.freeCurrentPotential J x + (minkowskiProduct c) (J x)) =
  kineticTerm 𝓕 A x - A.freeCurrentPotential J x - (minkowskiProduct c) (J x) kineticTerm_add_const,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 A x - { val := fun x => A.val x + c }.freeCurrentPotential J x =
  kineticTerm 𝓕 A x - A.freeCurrentPotential J x - (minkowskiProduct c) (J x)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 A x - (A.freeCurrentPotential J x + (minkowskiProduct c) (J x)) =
  kineticTerm 𝓕 A x - A.freeCurrentPotential J x - (minkowskiProduct c) (J x) freeCurrentPotential_add_constd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 A x - (A.freeCurrentPotential J x + (minkowskiProduct c) (J x)) =
  kineticTerm 𝓕 A x - A.freeCurrentPotential J x - (minkowskiProduct c) (J x)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 A x - (A.freeCurrentPotential J x + (minkowskiProduct c) (J x)) =
  kineticTerm 𝓕 A x - A.freeCurrentPotential J x - (minkowskiProduct c) (J x)]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dJ:LorentzCurrentDensity dc:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 A x - (A.freeCurrentPotential J x + (minkowskiProduct c) (J x)) =
  kineticTerm 𝓕 A x - A.freeCurrentPotential J x - (minkowskiProduct c) (J x)
  ringAll goals completed! 🐙

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

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


lemma lagrangian_eq_electric_magnetic {d} {𝓕 : FreeSpace}
    (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A)
    (J : LorentzCurrentDensity d) (x : SpaceTime d) :
    A.lagrangian 𝓕 J x = 1 / 2 * (𝓕.ε₀ * ‖A.electricField 𝓕.c (x.time 𝓕.c) x.space‖ ^ 2 -
    (1 / (2 * 𝓕.μ₀)) * ∑ i, ∑ j, ‖A.magneticFieldMatrix 𝓕.c (x.time 𝓕.c) x.space (i, j)‖ ^ 2)
    - A.scalarPotential 𝓕.c (x.time 𝓕.c) x.space * J.chargeDensity 𝓕.c (x.time 𝓕.c) x.space
    + ∑ i, A.vectorPotential 𝓕.c (x.time 𝓕.c) x.space i *
        J.currentDensity 𝓕.c (x.time 𝓕.c) x.space i := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ lagrangian 𝓕 A J x =
  1 / 2 *
        (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
          1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i
  rw [lagrangian,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ kineticTerm 𝓕 A x - A.freeCurrentPotential J x =
  1 / 2 *
        (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
          1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp id:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 2 *
      (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
        1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
    (scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
      ∑ i,
        (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) =
  1 / 2 *
        (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
          1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i
    kineticTerm_eq_electricMatrix_magneticFieldMatrix _ _ (hA.differentiable (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 2 ≠ 0d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 2 *
      (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
        1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
    (scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
      ∑ i,
        (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) =
  1 / 2 *
        (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
          1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i simpAll goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 2 *
      (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
        1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
    (scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
      ∑ i,
        (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) =
  1 / 2 *
        (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
          1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i)),
    freeCurrentPotential_eq_sum_scalarPotential_vectorPotential 𝓕 A J xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 2 *
      (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
        1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
    (scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
      ∑ i,
        (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) =
  1 / 2 *
        (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
          1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp id:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 2 *
      (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
        1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
    (scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
      ∑ i,
        (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) =
  1 / 2 *
        (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
          1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 2 *
      (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
        1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
    (scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
      ∑ i,
        (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) =
  1 / 2 *
        (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
          1 / (2 * 𝓕.μ₀) * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) -
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
    ∑ i,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i
  ringAll goals completed! 🐙

C. The variational gradient of the lagrangian density

C.1. The lagrangian density has a variational gradient



lemma lagrangian_hasVarGradientAt_eq_add_gradKineticTerm {𝓕 : FreeSpace}
    (A : ElectromagneticPotential d) (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d)
    (hJ : ContDiff ℝ ∞ J) :
    HasVarGradientAt (fun A => lagrangian 𝓕 ⟨A⟩ J)
    (A.gradKineticTerm 𝓕 - A.gradFreeCurrentPotential J) A := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun A => lagrangian 𝓕 { val := A } J) (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) A.val
  conv =>d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J| HasVarGradientAt (fun A => lagrangian 𝓕 { val := A } J) (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) A.val
    enter [1, q', x]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jq':SpaceTime d → Lorentz.Vector dx:SpaceTime d| lagrangian 𝓕 { val := q' } J x
    rw [lagrangian]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jq':SpaceTime d → Lorentz.Vector dx:SpaceTime d| kineticTerm 𝓕 { val := q' } x - { val := q' }.freeCurrentPotential J x
  apply HasVarGradientAt.addhd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun q' => kineticTerm 𝓕 { val := q' }) (gradKineticTerm 𝓕 A) A.valh'd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun q' x => -{ val := q' }.freeCurrentPotential J x)
  (fun i i_1 => -A.gradFreeCurrentPotential J i i_1) A.val
  ·hd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun q' => kineticTerm 𝓕 { val := q' }) (gradKineticTerm 𝓕 A) A.val exact A.kineticTerm_hasVarGradientAt hAAll goals completed! 🐙
  apply HasVarGradientAt.negh'd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun q' => { val := q' }.freeCurrentPotential J) (A.gradFreeCurrentPotential J) A.val
  convert freeCurrentPotential_hasVarGradientAt A hA J hJd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ A.gradFreeCurrentPotential J = ∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ
  rw [← gradFreeCurrentPotential_eq_sum_basis A hA J hJd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ A.gradFreeCurrentPotential J = A.gradFreeCurrentPotential JAll goals completed! 🐙]All goals completed! 🐙

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

lemma gradLagrangian_eq_kineticTerm_sub {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d)
    (hJ : ContDiff ℝ ∞ J) :
    A.gradLagrangian 𝓕 J = A.gradKineticTerm 𝓕 - A.gradFreeCurrentPotential J := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ gradLagrangian 𝓕 A J = gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J
  exact (lagrangian_hasVarGradientAt_eq_add_gradKineticTerm A hA J hJ).varGradientAll goals completed! 🐙

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


lemma lagrangian_hasVarGradientAt_gradLagrangian {𝓕 : FreeSpace}
    (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ ∞ J) :
    HasVarGradientAt (fun A => lagrangian 𝓕 ⟨A⟩ J) (A.gradLagrangian 𝓕 J) A := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun A => lagrangian 𝓕 { val := A } J) (gradLagrangian 𝓕 A J) A.val
  rw [gradLagrangian_eq_kineticTerm_sub A hA J hJd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun A => lagrangian 𝓕 { val := A } J) (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) A.vald:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun A => lagrangian 𝓕 { val := A } J) (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) A.val]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ HasVarGradientAt (fun A => lagrangian 𝓕 { val := A } J) (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) A.val
  apply lagrangian_hasVarGradientAt_eq_add_gradKineticTerm A hA J hJAll goals completed! 🐙

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



lemma gradLagrangian_eq_sum_fieldStrengthMatrix {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ ∞ J) :
    A.gradLagrangian 𝓕 J = fun x => ∑ ν,
      (η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν)
      • Lorentz.Vector.basis ν) := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ gradLagrangian 𝓕 A J = fun x =>
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis ν
  rw [gradLagrangian_eq_kineticTerm_sub A hA J hJd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J = fun x =>
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis νd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J = fun x =>
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis ν]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ J⊢ gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J = fun x =>
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis ν
  funext xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) x =
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis ν
  simp only [Pi.sub_apply]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ gradKineticTerm 𝓕 A x - A.gradFreeCurrentPotential J x =
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis ν
  rw [gradKineticTerm_eq_fieldStrength,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ ν, (1 / 𝓕.μ₀ * η ν ν) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν -
    A.gradFreeCurrentPotential J x =
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis νhad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.vald:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ ν, (1 / 𝓕.μ₀ * η ν ν) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν -
    (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x =
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis νhad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.val gradFreeCurrentPotential_eq_sum_basis A hA J hJd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ ν, (1 / 𝓕.μ₀ * η ν ν) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν -
    (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x =
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis νhad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.vald:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ ν, (1 / 𝓕.μ₀ * η ν ν) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν -
    (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x =
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis νhad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.val]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ ν, (1 / 𝓕.μ₀ * η ν ν) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν -
    (∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ) x =
  ∑ ν, η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis νhad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.val
  simp only [one_div, Finset.sum_apply]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ x_1, (𝓕.μ₀⁻¹ * η x_1 x_1) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x) • Lorentz.Vector.basis x_1 -
    ∑ c, (η c c * J x c) • Lorentz.Vector.basis c =
  ∑ x_1,
    η x_1 x_1 •
      (𝓕.μ₀⁻¹ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x - J x x_1) • Lorentz.Vector.basis x_1had:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.val
  rw [← Finset.sum_sub_distribd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ x_1,
    ((𝓕.μ₀⁻¹ * η x_1 x_1) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x) • Lorentz.Vector.basis x_1 -
      (η x_1 x_1 * J x x_1) • Lorentz.Vector.basis x_1) =
  ∑ x_1,
    η x_1 x_1 •
      (𝓕.μ₀⁻¹ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x - J x x_1) • Lorentz.Vector.basis x_1had:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.vald:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ x_1,
    ((𝓕.μ₀⁻¹ * η x_1 x_1) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x) • Lorentz.Vector.basis x_1 -
      (η x_1 x_1 * J x x_1) • Lorentz.Vector.basis x_1) =
  ∑ x_1,
    η x_1 x_1 •
      (𝓕.μ₀⁻¹ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x - J x x_1) • Lorentz.Vector.basis x_1had:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.val]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ x_1,
    ((𝓕.μ₀⁻¹ * η x_1 x_1) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x) • Lorentz.Vector.basis x_1 -
      (η x_1 x_1 * J x x_1) • Lorentz.Vector.basis x_1) =
  ∑ x_1,
    η x_1 x_1 •
      (𝓕.μ₀⁻¹ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, x_1)) x - J x x_1) • Lorentz.Vector.basis x_1had:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.val
  refine Finset.sum_congr rfl (fun ν _ => ?_)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ (𝓕.μ₀⁻¹ * η ν ν) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν -
    (η ν ν * J x ν) • Lorentz.Vector.basis ν =
  η ν ν • (𝓕.μ₀⁻¹ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν) • Lorentz.Vector.basis νhad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.val
  modulehad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ContDiff ℝ ∞ A.val
  exact hAAll goals completed! 🐙

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


lemma gradLagrangian_eq_electricField_magneticField {𝓕 : FreeSpace}
    (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d)
    (hJ : ContDiff ℝ ∞ J) (x : SpaceTime d) :
    A.gradLagrangian 𝓕 J x = (1 / (𝓕.μ₀ * 𝓕.c.val) *
        Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        - 𝓕.c * J.chargeDensity 𝓕.c (x.time 𝓕.c) x.space) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i, (𝓕.μ₀⁻¹ * (𝓕.ε₀ * 𝓕.μ₀ * ∂ₜ (electricField 𝓕.c A · x.space) ((time 𝓕.c) x) i -
      ∑ j, ∂[j] (magneticFieldMatrix 𝓕.c A (x.time 𝓕.c) · (j, i)) x.space) +
      J.currentDensity 𝓕.c (x.time 𝓕.c) x.space i) •
        Lorentz.Vector.basis (Sum.inr i) := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ gradLagrangian 𝓕 A J x =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)
  rw [gradLagrangian_eq_kineticTerm_sub A hA J hJ,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) x =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      ((𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
              ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
          Lorentz.Vector.basis (Sum.inr x_1) -
        -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i) Pi.sub_apply,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ gradKineticTerm 𝓕 A x - A.gradFreeCurrentPotential J x =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      ((𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
              ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
          Lorentz.Vector.basis (Sum.inr x_1) -
        -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)
    gradKineticTerm_eq_electric_magnetic _ _ hA,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
      ∑ i,
        (𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
          Lorentz.Vector.basis (Sum.inr i) -
    A.gradFreeCurrentPotential J x =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      ((𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
              ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
          Lorentz.Vector.basis (Sum.inr x_1) -
        -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)
    gradFreeCurrentPotential_eq_chargeDensity_currentDensity 𝓕 A hA J hJ x,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
      ∑ i,
        (𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
          Lorentz.Vector.basis (Sum.inr i) -
    ((𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
      ∑ i, -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      ((𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
              ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
          Lorentz.Vector.basis (Sum.inr x_1) -
        -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)
    add_sub_add_comm,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    (∑ i,
        (𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
          Lorentz.Vector.basis (Sum.inr i) -
      ∑ i, -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      ((𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
              ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
          Lorentz.Vector.basis (Sum.inr x_1) -
        -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i) ← Finset.sum_sub_distribd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      ((𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
              ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
          Lorentz.Vector.basis (Sum.inr x_1) -
        -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      ((𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
              ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
          Lorentz.Vector.basis (Sum.inr x_1) -
        -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
      (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) +
    ∑ x_1,
      ((𝓕.μ₀⁻¹ *
            (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
              ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
          Lorentz.Vector.basis (Sum.inr x_1) -
        -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
        -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
      Lorentz.Vector.basis (Sum.inl 0) +
    ∑ i,
      (𝓕.μ₀⁻¹ *
            (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
              ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
          (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
        Lorentz.Vector.basis (Sum.inr i)
  congr 1e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
    (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
      -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
    Lorentz.Vector.basis (Sum.inl 0)e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ x_1,
    ((𝓕.μ₀⁻¹ *
          (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
            ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
        Lorentz.Vector.basis (Sum.inr x_1) -
      -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  ∑ i,
    (𝓕.μ₀⁻¹ *
          (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
            ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
        (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
      Lorentz.Vector.basis (Sum.inr i)
  ·e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x)) • Lorentz.Vector.basis (Sum.inl 0) -
    (𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) • Lorentz.Vector.basis (Sum.inl 0) =
  (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((time 𝓕.c) x)) (space x) +
      -𝓕.c.val * chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x)) •
    Lorentz.Vector.basis (Sum.inl 0) moduleAll goals completed! 🐙
  ·e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime d⊢ ∑ x_1,
    ((𝓕.μ₀⁻¹ *
          (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp x_1 -
            ∑ j, Space.deriv j (fun x_2 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_2 (j, x_1)) (space x))) •
        Lorentz.Vector.basis (Sum.inr x_1) -
      -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1 • Lorentz.Vector.basis (Sum.inr x_1)) =
  ∑ i,
    (𝓕.μ₀⁻¹ *
          (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
            ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
        (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
      Lorentz.Vector.basis (Sum.inr i) refine Finset.sum_congr rfl fun i _ => ?_e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime di:Fin dx✝:i ∈ Finset.univ⊢ (𝓕.μ₀⁻¹ *
        (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
      Lorentz.Vector.basis (Sum.inr i) -
    -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i) =
  (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
      (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
    Lorentz.Vector.basis (Sum.inr i)
    rw [𝓕.c_sq,e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime di:Fin dx✝:i ∈ Finset.univ⊢ (𝓕.μ₀⁻¹ *
        (1 / (1 / (𝓕.ε₀ * 𝓕.μ₀)) * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
      Lorentz.Vector.basis (Sum.inr i) -
    -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i) =
  (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
      (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
    Lorentz.Vector.basis (Sum.inr i)e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime di:Fin dx✝:i ∈ Finset.univ⊢ (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
      Lorentz.Vector.basis (Sum.inr i) -
    -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i) =
  (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
      (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
    Lorentz.Vector.basis (Sum.inr i) one_div_one_dive_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime di:Fin dx✝:i ∈ Finset.univ⊢ (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
      Lorentz.Vector.basis (Sum.inr i) -
    -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i) =
  (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
      (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
    Lorentz.Vector.basis (Sum.inr i)e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime di:Fin dx✝:i ∈ Finset.univ⊢ (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
      Lorentz.Vector.basis (Sum.inr i) -
    -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i) =
  (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
      (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
    Lorentz.Vector.basis (Sum.inr i)]e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime di:Fin dx✝:i ∈ Finset.univ⊢ (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x))) •
      Lorentz.Vector.basis (Sum.inr i) -
    -(currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i • Lorentz.Vector.basis (Sum.inr i) =
  (𝓕.μ₀⁻¹ *
        (𝓕.ε₀ * 𝓕.μ₀ * (∂ₜ (fun x_1 => electricField 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
          ∑ j, Space.deriv j (fun x_1 => magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) x_1 (j, i)) (space x)) +
      (currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp i) •
    Lorentz.Vector.basis (Sum.inr i)
    moduleAll goals completed! 🐙

C.7. The lagrangian gradient in tensor notation


attribute [-simp] Nat.reduceAdd Nat.reduceSucc Fin.isValue in
lemma gradLagrangian_eq_tensor {𝓕 : FreeSpace}
    (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d)
    (hJ : ContDiff ℝ ∞ J) (x : SpaceTime d) (ν : Fin 1 ⊕ Fin d) :
    A.gradLagrangian 𝓕 J x ν =
    η ν ν * ((Tensorial.toTensor (M := Lorentz.Vector d)).symm
    (permT id (IsReindexing.auto) {((1/ 𝓕.μ₀ : ℝ) • tensorDeriv A.toFieldStrength x | κ κ ν') +
    - (J x | ν')}ᵀ)) ν := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ gradLagrangian 𝓕 A J x ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯)
        ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)) +
          (permT ![0] ⋯) (-Tensorial.toTensor (J x))))
      ν
  rw [gradLagrangian_eq_kineticTerm_sub _ hA _ hJd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) x ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯)
        ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)) +
          (permT ![0] ⋯) (-Tensorial.toTensor (J x))))
      νd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) x ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯)
        ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)) +
          (permT ![0] ⋯) (-Tensorial.toTensor (J x))))
      ν]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ (gradKineticTerm 𝓕 A - A.gradFreeCurrentPotential J) x ν =
  η ν ν *
    Tensorial.toTensor.symm
      ((permT id ⋯)
        ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)) +
          (permT ![0] ⋯) (-Tensorial.toTensor (J x))))
      ν
  simp only [Pi.sub_apply, apply_sub, one_div, map_smul,
    map_neg, map_add, permT_permT, CompTriple.comp_eq, apply_add, apply_smul,
    Lorentz.Vector.neg_apply]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ gradKineticTerm 𝓕 A x ν - A.gradFreeCurrentPotential J x ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν +
      -Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν)
  rw [gradKineticTerm_eq_tensorDeriv A x hAd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν *
      Tensorial.toTensor.symm
        ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)))) ν -
    A.gradFreeCurrentPotential J x ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν +
      -Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν *
      Tensorial.toTensor.symm
        ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)))) ν -
    A.gradFreeCurrentPotential J x ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν +
      -Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν)]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν *
      Tensorial.toTensor.symm
        ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)))) ν -
    A.gradFreeCurrentPotential J x ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν +
      -Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν)
  rw [gradFreeCurrentPotential_eq_tensor A hA J hJ x νd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν *
      Tensorial.toTensor.symm
        ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)))) ν -
    η ν ν * Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))) ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν +
      -Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν *
      Tensorial.toTensor.symm
        ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)))) ν -
    η ν ν * Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))) ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν +
      -Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν)]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν *
      Tensorial.toTensor.symm
        ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor ((1 / 𝓕.μ₀) • tensorDeriv A.toFieldStrength x)))) ν -
    η ν ν * Tensorial.toTensor.symm ((permT id ⋯) (Tensorial.toTensor (J x))) ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν +
      -Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν)
  simp only [one_div, map_smul, apply_smul,
    permT_id_self, LinearEquiv.symm_apply_apply]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν *
      (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν) -
    η ν ν * J x ν =
  η ν ν *
    (𝓕.μ₀⁻¹ *
        Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
          ν +
      -Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν)
  ring_nfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ η ν ν * 𝓕.μ₀⁻¹ *
      Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
        ν -
    η ν ν * J x ν =
  η ν ν * 𝓕.μ₀⁻¹ *
      Tensorial.toTensor.symm ((permT id ⋯) ((contrT 1 0 1 ⋯) (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))))
        ν -
    η ν ν * Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν
  congre_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ J x ν = Tensorial.toTensor.symm ((permT ![0] ⋯) (Tensorial.toTensor (J x))) ν
  rw [permT_congr_eq_ide_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ J x ν = Tensorial.toTensor.symm (Tensorial.toTensor (J x)) νe_a.e_a.hd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ ![0] = ide_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ J x ν = Tensorial.toTensor.symm (Tensorial.toTensor (J x)) νe_a.e_a.hd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ ![0] = id]e_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ J x ν = Tensorial.toTensor.symm (Tensorial.toTensor (J x)) νe_a.e_a.hd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ ![0] = id
  simp only [LinearEquiv.symm_apply_apply]e_a.e_a.hd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ ![0] = id
  funext ie_a.e_a.hd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin di:Fin (Nat.succ 0)⊢ ![0] i = id i
  fin_cases ie_a.e_a.h.«_@»._internal._hyg.0.«0»d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valJ:LorentzCurrentDensity dhJ:ContDiff ℝ ∞ Jx:SpaceTime dν:Fin 1 ⊕ Fin d⊢ ![0] ((fun i => i) ⟨0, ⋯⟩) = id ((fun i => i) ⟨0, ⋯⟩)
  simpAll goals completed! 🐙

The Lagrangian in electromagnetism

i. Overview

ii. Key results

iii. Table of contents

iv. References

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

C.7. The lagrangian gradient in tensor notation

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

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