Physlib.Electromagnetism.Dynamics.Hamiltonian — Physlib

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.Lagrangian

The Hamiltonian in electromagnetism

i. Overview

In this module we define the canonical momentum and the Hamiltonian for the electromagnetic field in presence of a current density. We prove properties of these quantities, and express the Hamiltonian in terms of the electric and magnetic fields in the case of three spatial dimensions.

ii. Key results

canonicalMomentum : The canonical momentum for the electromagnetic field in presence of a Lorentz current density.

hamiltonian : The Hamiltonian for the electromagnetic field in presence of a Lorentz current density.

hamiltonian_eq_electricField_magneticField : The Hamiltonian expressed in terms of the electric and magnetic fields.

iii. Table of contents

A. The canonical momentum

A.1. The canonical momentum in terms of the kinetic term

A.2. The canonical momentum in terms of the field strength tensor

A.3. The canonical momentum in terms of the electric field

B. The Hamiltonian

B.1. The hamiltonian in terms of the vector potential

B.2. The hamiltonian in terms of the electric and magnetic fields

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. The canonical momentum

We define the canonical momentum for the lagrangian L(A, ∂ A) as gradient of v ↦ L(A + t v, ∂ (A + t v)) - t * L(A + v, ∂(A + v)) at v = 0 This is equivalent to ∂ L/∂ (∂_0 A).

A.1. The canonical momentum in terms of the kinetic term


lemma canonicalMomentum_eq_gradient_kineticTerm {d}
    {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) :
    A.canonicalMomentum 𝓕 J = fun x =>
    gradient (fun (v : Lorentz.Vector d) =>
    kineticTerm 𝓕 ⟨fun x => A x + x (Sum.inl 0) • v⟩ x) 0:= byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ canonicalMomentum 𝓕 A J = fun x => gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0
  funext xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ canonicalMomentum 𝓕 A J x = gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0
  apply ext_inner_right (𝕜 := ℝ)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∀ (v : Lorentz.Vector d),
  ⟪canonicalMomentum 𝓕 A J x, v⟫_ℝ =
    ⟪gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0, v⟫_ℝ
  intro vd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪canonicalMomentum 𝓕 A J x, v⟫_ℝ =
  ⟪gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0, v⟫_ℝ
  rw [gradient,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪canonicalMomentum 𝓕 A J x, v⟫_ℝ =
  ⟪(toDual ℝ (Lorentz.Vector d)).symm
      (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0),
    v⟫_ℝd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0 -
      x (Sum.inl 0) • gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0,
    v⟫_ℝ =
  ⟪(toDual ℝ (Lorentz.Vector d)).symm
      (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0),
    v⟫_ℝ canonicalMomentumd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0 -
      x (Sum.inl 0) • gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0,
    v⟫_ℝ =
  ⟪(toDual ℝ (Lorentz.Vector d)).symm
      (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0),
    v⟫_ℝd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0 -
      x (Sum.inl 0) • gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0,
    v⟫_ℝ =
  ⟪(toDual ℝ (Lorentz.Vector d)).symm
      (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0),
    v⟫_ℝ]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0 -
      x (Sum.inl 0) • gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0,
    v⟫_ℝ =
  ⟪(toDual ℝ (Lorentz.Vector d)).symm
      (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0),
    v⟫_ℝ
  simp only [Fin.isValue, toDual_symm_apply]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0 -
      x (Sum.inl 0) • gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0,
    v⟫_ℝ =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v
  rw [inner_sub_left,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0, v⟫_ℝ -
    ⟪x (Sum.inl 0) • gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0, v⟫_ℝ =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) vd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0, v⟫_ℝ -
    (starRingEnd ℝ) (x (Sum.inl 0)) * ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0, v⟫_ℝ =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v inner_smul_leftd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0, v⟫_ℝ -
    (starRingEnd ℝ) (x (Sum.inl 0)) * ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0, v⟫_ℝ =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) vd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0, v⟫_ℝ -
    (starRingEnd ℝ) (x (Sum.inl 0)) * ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0, v⟫_ℝ =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0, v⟫_ℝ -
    (starRingEnd ℝ) (x (Sum.inl 0)) * ⟪gradient (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0, v⟫_ℝ =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v
  simp [gradient]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ (fderiv ℝ (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v
  conv_lhs =>
    enter [2]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d| x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 { val := fun x => A.val x + v } J x) 0) v
    simp [lagrangian_add_const]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d| x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x - (minkowskiProduct v) (J x)) 0) v
  have hx : DifferentiableAt ℝ (fun v => kineticTerm 𝓕 ⟨fun x => A x + x (Sum.inl 0) • v⟩ x) 0 := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ canonicalMomentum 𝓕 A J = fun x => gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x - (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v
    simp only [kineticTerm_add_time_mul_const _ (hA.differentiable (by simp))]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ DifferentiableAt ℝ
  (fun v =>
    kineticTerm 𝓕 A x +
      (-1 / (2 * 𝓕.μ₀) *
          ∑ ν, (2 * v ν * η ν ν * ∂_ (Sum.inl 0) A.val x ν + η ν ν * v ν ^ 2 - 2 * v ν * ∂_ ν A.val x (Sum.inl 0)) +
        1 / (2 * 𝓕.μ₀) * v (Sum.inl 0) ^ 2))
  0d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x - (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v
    fun_propd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x - (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) vd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x - (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v
  conv_lhs =>
    enter [1]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0| (fderiv ℝ (fun v => lagrangian 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } J x) 0) v
    simp only [lagrangian, Fin.isValue, map_add, map_smul,
      LinearMap.smul_apply, smul_eq_mul]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0| (fderiv ℝ
    (fun v =>
      kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x -
        { val := fun x => A.val x + x (Sum.inl 0) • v }.freeCurrentPotential J x)
    0)
  v
    rw [fderiv_fun_sub hx (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ DifferentiableAt ℝ (fun v => { val := fun x => A.val x + x (Sum.inl 0) • v }.freeCurrentPotential J x) 0 simp [freeCurrentPotential]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ DifferentiableAt ℝ (fun y => x (Sum.inl 0) * (minkowskiProduct y) (J x)) 0; fun_propAll goals completed! 🐙)]
    simp only [Fin.isValue, freeCurrentPotential, map_add, map_smul, _root_.add_apply,
      FunLike.coe_smul, Pi.smul_apply, smul_eq_mul, fderiv_const_add,
      FunLike.coe_sub, Pi.sub_apply]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0| (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v -
  (fderiv ℝ (fun y => x (Sum.inl 0) * (minkowskiProduct y) (J x)) 0) v
    rw [fderiv_const_mul (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ DifferentiableAt ℝ (fun y => (minkowskiProduct y) (J x)) 0 fun_propAll goals completed! 🐙)]
  simp only [Fin.isValue, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v -
      x (Sum.inl 0) * (fderiv ℝ (fun y => (minkowskiProduct y) (J x)) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x - (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v
  rw [fderiv_fun_sub (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ DifferentiableAt ℝ (fun v => lagrangian 𝓕 A J x) 0d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v -
      x (Sum.inl 0) * (fderiv ℝ (fun y => (minkowskiProduct y) (J x)) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x) 0 - fderiv ℝ (fun v => (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v -
      x (Sum.inl 0) * (fderiv ℝ (fun y => (minkowskiProduct y) (J x)) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x) 0 - fderiv ℝ (fun v => (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v) (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ DifferentiableAt ℝ (fun v => (minkowskiProduct v) (J x)) 0d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v -
      x (Sum.inl 0) * (fderiv ℝ (fun y => (minkowskiProduct y) (J x)) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x) 0 - fderiv ℝ (fun v => (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v fun_propAll goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v -
      x (Sum.inl 0) * (fderiv ℝ (fun y => (minkowskiProduct y) (J x)) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x) 0 - fderiv ℝ (fun v => (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v)]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dhx:DifferentiableAt ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0⊢ (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v -
      x (Sum.inl 0) * (fderiv ℝ (fun y => (minkowskiProduct y) (J x)) 0) v -
    x (Sum.inl 0) * (fderiv ℝ (fun v => lagrangian 𝓕 A J x) 0 - fderiv ℝ (fun v => (minkowskiProduct v) (J x)) 0) v =
  (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v
  simpAll goals completed! 🐙

A.2. The canonical momentum in terms of the field strength tensor



lemma canonicalMomentum_eq {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) :
    A.canonicalMomentum 𝓕 J = fun x => fun μ =>
      (1/𝓕.μ₀) * η μ μ • A.fieldStrengthMatrix x (μ, Sum.inl 0) := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ canonicalMomentum 𝓕 A J = fun x μ => 1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)
  rw [canonicalMomentum_eq_gradient_kineticTerm A hA Jd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ (fun x => gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) = fun x μ =>
  1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ (fun x => gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) = fun x μ =>
  1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ (fun x => gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) = fun x μ =>
  1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)
  funext xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0 = fun μ =>
  1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)
  apply ext_inner_right (𝕜 := ℝ)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∀ (v : Lorentz.Vector d),
  ⟪gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0, v⟫_ℝ =
    ⟪fun μ => 1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0), v⟫_ℝ
  intro vd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ⟪gradient (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0, v⟫_ℝ =
  ⟪fun μ => 1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0), v⟫_ℝ
  simp [gradient]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ (fderiv ℝ (fun v => kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x) 0) v =
  ⟪fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)), v⟫_ℝ
  conv_lhs =>
    enter [1, 2, v]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv✝:Lorentz.Vector dv:Lorentz.Vector d| kineticTerm 𝓕 { val := fun x => A.val x + x (Sum.inl 0) • v } x
    rw [kineticTerm_add_time_mul_const _ (hA.differentiable (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv✝:Lorentz.Vector dv:Lorentz.Vector d⊢ 2 ≠ 0 simpAll goals completed! 🐙))]
  simp (disch := fun_prop) only [Fin.isValue, Finset.sum_sub_distrib, one_div,
    fderiv_const_add, fderiv_fun_add, fderiv_const_mul, fderiv_fun_sub, fderiv_fun_sum,
    fderiv_mul_const, fderiv_fun_pow]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ((-1 / (2 * 𝓕.μ₀)) •
        (∑ x_1,
            (∂_ (Sum.inl 0) A.val x x_1 • η x_1 x_1 • 2 • fderiv ℝ (fun y => y x_1) 0 +
              η x_1 x_1 • (2 • 0 x_1 ^ (2 - 1)) • fderiv ℝ (fun y => y x_1) 0) -
          ∑ x_1, ∂_ x_1 A.val x (Sum.inl 0) • 2 • fderiv ℝ (fun y => y x_1) 0) +
      (2 * 𝓕.μ₀)⁻¹ • (2 • 0 (Sum.inl 0) ^ (2 - 1)) • fderiv ℝ (fun i => i (Sum.inl 0)) 0)
    v =
  ⟪fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)), v⟫_ℝ
  simp [Lorentz.Vector.coordCLM]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ -1 / (2 * 𝓕.μ₀) *
    (∑ x_1, ∂_ (Sum.inl 0) A.val x x_1 * (η x_1 x_1 * (2 * v x_1)) - ∑ x_1, ∂_ x_1 A.val x (Sum.inl 0) * (2 * v x_1)) =
  ⟪fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)), v⟫_ℝ
  rw [← Finset.sum_sub_distrib,d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ -1 / (2 * 𝓕.μ₀) *
    ∑ x_1, (∂_ (Sum.inl 0) A.val x x_1 * (η x_1 x_1 * (2 * v x_1)) - ∂_ x_1 A.val x (Sum.inl 0) * (2 * v x_1)) =
  ⟪fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)), v⟫_ℝd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ∑ i, -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x i * (η i i * (2 * v i)) - ∂_ i A.val x (Sum.inl 0) * (2 * v i)) =
  ⟪fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)), v⟫_ℝ Finset.mul_sumd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ∑ i, -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x i * (η i i * (2 * v i)) - ∂_ i A.val x (Sum.inl 0) * (2 * v i)) =
  ⟪fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)), v⟫_ℝd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ∑ i, -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x i * (η i i * (2 * v i)) - ∂_ i A.val x (Sum.inl 0) * (2 * v i)) =
  ⟪fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)), v⟫_ℝ]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ ∑ i, -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x i * (η i i * (2 * v i)) - ∂_ i A.val x (Sum.inl 0) * (2 * v i)) =
  ⟪fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)), v⟫_ℝ
  congre_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector d⊢ (fun i => -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x i * (η i i * (2 * v i)) - ∂_ i A.val x (Sum.inl 0) * (2 * v i))) =
  fun i =>
  ⟪((equivEuclid d) fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0))).ofLp i,
    ((equivEuclid d) v).ofLp i⟫_ℝ
  ext μe_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x μ * (η μ μ * (2 * v μ)) - ∂_ μ A.val x (Sum.inl 0) * (2 * v μ)) =
  ⟪((equivEuclid d) fun μ => 𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0))).ofLp μ,
    ((equivEuclid d) v).ofLp μ⟫_ℝ
  simp only [Fin.isValue, RCLike.inner_apply, conj_trivial, equivEuclid_apply]e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x μ * (η μ μ * (2 * v μ)) - ∂_ μ A.val x (Sum.inl 0) * (2 * v μ)) =
  v μ * (𝓕.μ₀⁻¹ * (η μ μ * (A.fieldStrengthMatrix x) (μ, Sum.inl 0)))
  rw [fieldStrengthMatrix,e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x μ * (η μ μ * (2 * v μ)) - ∂_ μ A.val x (Sum.inl 0) * (2 * v μ)) =
  v μ *
    (𝓕.μ₀⁻¹ *
      (η μ μ * ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, Sum.inl 0)))e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x μ * (η μ μ * (2 * v μ)) - ∂_ μ A.val x (Sum.inl 0) * (2 * v μ)) =
  v μ *
    (𝓕.μ₀⁻¹ *
      (η μ μ *
        (η (μ, Sum.inl 0).1 (μ, Sum.inl 0).1 * ∂_ (μ, Sum.inl 0).1 A.val x (μ, Sum.inl 0).2 -
          η (μ, Sum.inl 0).2 (μ, Sum.inl 0).2 * ∂_ (μ, Sum.inl 0).2 A.val x (μ, Sum.inl 0).1))) toFieldStrength_basis_repr_apply_eq_singlee_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x μ * (η μ μ * (2 * v μ)) - ∂_ μ A.val x (Sum.inl 0) * (2 * v μ)) =
  v μ *
    (𝓕.μ₀⁻¹ *
      (η μ μ *
        (η (μ, Sum.inl 0).1 (μ, Sum.inl 0).1 * ∂_ (μ, Sum.inl 0).1 A.val x (μ, Sum.inl 0).2 -
          η (μ, Sum.inl 0).2 (μ, Sum.inl 0).2 * ∂_ (μ, Sum.inl 0).2 A.val x (μ, Sum.inl 0).1)))e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x μ * (η μ μ * (2 * v μ)) - ∂_ μ A.val x (Sum.inl 0) * (2 * v μ)) =
  v μ *
    (𝓕.μ₀⁻¹ *
      (η μ μ *
        (η (μ, Sum.inl 0).1 (μ, Sum.inl 0).1 * ∂_ (μ, Sum.inl 0).1 A.val x (μ, Sum.inl 0).2 -
          η (μ, Sum.inl 0).2 (μ, Sum.inl 0).2 * ∂_ (μ, Sum.inl 0).2 A.val x (μ, Sum.inl 0).1)))]e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x μ * (η μ μ * (2 * v μ)) - ∂_ μ A.val x (Sum.inl 0) * (2 * v μ)) =
  v μ *
    (𝓕.μ₀⁻¹ *
      (η μ μ *
        (η (μ, Sum.inl 0).1 (μ, Sum.inl 0).1 * ∂_ (μ, Sum.inl 0).1 A.val x (μ, Sum.inl 0).2 -
          η (μ, Sum.inl 0).2 (μ, Sum.inl 0).2 * ∂_ (μ, Sum.inl 0).2 A.val x (μ, Sum.inl 0).1)))
  simp only [Fin.isValue, inl_0_inl_0, one_mul]e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -1 / (2 * 𝓕.μ₀) * (∂_ (Sum.inl 0) A.val x μ * (η μ μ * (2 * v μ)) - ∂_ μ A.val x (Sum.inl 0) * (2 * v μ)) =
  v μ * (𝓕.μ₀⁻¹ * (η μ μ * (η μ μ * ∂_ μ A.val x (Sum.inl 0) - ∂_ (Sum.inl 0) A.val x μ)))
  ring_nfe_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dv:Lorentz.Vector dμ:Fin 1 ⊕ Fin d⊢ -(𝓕.μ₀⁻¹ * ∂_ (Sum.inl 0) A.val x μ * η μ μ * v μ) + 𝓕.μ₀⁻¹ * v μ * ∂_ μ A.val x (Sum.inl 0) =
  -(𝓕.μ₀⁻¹ * ∂_ (Sum.inl 0) A.val x μ * η μ μ * v μ) + 𝓕.μ₀⁻¹ * η μ μ ^ 2 * v μ * ∂_ μ A.val x (Sum.inl 0)
  simpAll goals completed! 🐙

A.3. The canonical momentum in terms of the electric field



lemma canonicalMomentum_eq_electricField {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) :
    A.canonicalMomentum 𝓕 J = fun x => fun μ =>
      match μ with
      | Sum.inl 0 => 0
      | Sum.inr i => - (1/(𝓕.μ₀ * 𝓕.c)) * A.electricField 𝓕.c (x.time 𝓕.c) x.space i := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ canonicalMomentum 𝓕 A J = fun x μ =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => -(1 / (𝓕.μ₀ * 𝓕.c.val)) * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i
  rw [canonicalMomentum_eq A hA Jd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ (fun x μ => 1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)) = fun x μ =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => -(1 / (𝓕.μ₀ * 𝓕.c.val)) * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp id:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ (fun x μ => 1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)) = fun x μ =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => -(1 / (𝓕.μ₀ * 𝓕.c.val)) * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity d⊢ (fun x μ => 1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)) = fun x μ =>
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => -(1 / (𝓕.μ₀ * 𝓕.c.val)) * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i
  funext x μd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ 1 / 𝓕.μ₀ * η μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0) =
  match μ with
  | Sum.inl 0 => 0
  | Sum.inr i => -(1 / (𝓕.μ₀ * 𝓕.c.val)) * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i
  match μ with
  | Sum.inl 0 =>d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ 1 / 𝓕.μ₀ * η (Sum.inl 0) (Sum.inl 0) • (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inl 0) =
  match Sum.inl 0 with
  | Sum.inl 0 => 0
  | Sum.inr i => -(1 / (𝓕.μ₀ * 𝓕.c.val)) * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i simpAll goals completed! 🐙
  | Sum.inr i =>d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ 1 / 𝓕.μ₀ * η (Sum.inr i) (Sum.inr i) • (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inl 0) =
  match Sum.inr i with
  | Sum.inl 0 => 0
  | Sum.inr i => -(1 / (𝓕.μ₀ * 𝓕.c.val)) * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i
  simp only [one_div, inr_i_inr_i, Fin.isValue, smul_eq_mul, neg_mul, one_mul, mul_neg, mul_inv_rev,
    neg_inj]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ 𝓕.μ₀⁻¹ * (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inl 0) =
  𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i
  rw [electricField_eq_fieldStrengthMatrix (hA := hA.differentiable (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin dt✝:Timex✝:Space di✝:Fin d⊢ 2 ≠ 0d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ 𝓕.μ₀⁻¹ * (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inl 0) =
  𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
    (-𝓕.c.val * (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm ((time 𝓕.c) x, space x))) (Sum.inl 0, Sum.inr i)) simpAll goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ 𝓕.μ₀⁻¹ * (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inl 0) =
  𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
    (-𝓕.c.val * (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm ((time 𝓕.c) x, space x))) (Sum.inl 0, Sum.inr i))))]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ 𝓕.μ₀⁻¹ * (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inl 0) =
  𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ *
    (-𝓕.c.val * (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm ((time 𝓕.c) x, space x))) (Sum.inl 0, Sum.inr i))
  simp only [Fin.isValue, toTimeAndSpace_symm_apply_time_space, neg_mul, mul_neg]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ 𝓕.μ₀⁻¹ * (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inl 0) =
  -(𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (𝓕.c.val * (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i)))
  field_simpd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime dμ:Fin 1 ⊕ Fin di:Fin d⊢ (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inl 0) = -(A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i)
  exact fieldStrengthMatrix_antisymm A x (Sum.inr i) (Sum.inl 0)All goals completed! 🐙

B. The Hamiltonian

B.1. The hamiltonian in terms of the vector potential



lemma hamiltonian_eq_electricField_vectorPotential {d} {𝓕 : FreeSpace}
    (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A)
    (J : LorentzCurrentDensity d) (x : SpaceTime d) :
    A.hamiltonian 𝓕 J x =
      - (1/ 𝓕.c.val^2 * 𝓕.μ₀⁻¹) * ∑ i, A.electricField 𝓕.c (x.time 𝓕.c) x.space i *
      (∂ₜ (A.vectorPotential 𝓕.c · x.space) (x.time 𝓕.c) i) - lagrangian 𝓕 A J x := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ hamiltonian 𝓕 A J x =
  -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
      ∑ i,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
    lagrangian 𝓕 A J x
  rw [hamiltoniand:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ μ, canonicalMomentum 𝓕 A J x μ * ∂_ (Sum.inl 0) A.val x μ - lagrangian 𝓕 A J x =
  -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
      ∑ i,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
    lagrangian 𝓕 A J xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ μ, canonicalMomentum 𝓕 A J x μ * ∂_ (Sum.inl 0) A.val x μ - lagrangian 𝓕 A J x =
  -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
      ∑ i,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
    lagrangian 𝓕 A J x]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ μ, canonicalMomentum 𝓕 A J x μ * ∂_ (Sum.inl 0) A.val x μ - lagrangian 𝓕 A J x =
  -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
      ∑ i,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
    lagrangian 𝓕 A J x
  congr 1e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ μ, canonicalMomentum 𝓕 A J x μ * ∂_ (Sum.inl 0) A.val x μ =
  -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
    ∑ i,
      (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i
  simp [Fintype.sum_sum_type, canonicalMomentum_eq_electricField A hA J]e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ x_1,
    𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
      ∂_ (Sum.inl 0) A.val x (Sum.inr x_1) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ∑ x_1,
      (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
        (∂ₜ (fun x_2 => vectorPotential 𝓕.c A x_2 (space x)) ((time 𝓕.c) x)).ofLp x_1
  rw [Finset.mul_sume_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ x_1,
    𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
      ∂_ (Sum.inl 0) A.val x (Sum.inr x_1) =
  ∑ i,
    (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i)e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ x_1,
    𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
      ∂_ (Sum.inl 0) A.val x (Sum.inr x_1) =
  ∑ i,
    (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i)]e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ ∑ x_1,
    𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
      ∂_ (Sum.inl 0) A.val x (Sum.inr x_1) =
  ∑ i,
    (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i)
  congre_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ (fun x_1 =>
    𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
      ∂_ (Sum.inl 0) A.val x (Sum.inr x_1)) =
  fun i =>
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i)
  funext ie_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i * ∂_ (Sum.inl 0) A.val x (Sum.inr i) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i)
  rw [SpaceTime.deriv_sum_inl 𝓕.ce_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    ((1 / 𝓕.c.val) •
        ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1)
      (Sum.inr i) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.vale_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    ((1 / 𝓕.c.val) •
        ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1)
      (Sum.inr i) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val]e_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    ((1 / 𝓕.c.val) •
        ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1)
      (Sum.inr i) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val
  rw [← Time.deriv_euclide_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    ((1 / 𝓕.c.val) •
        ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1)
      (Sum.inr i) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      ∂ₜ (fun t => (vectorPotential 𝓕.c A t (space x)).ofLp i) ((time 𝓕.c) x))e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.vale_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    ((1 / 𝓕.c.val) •
        ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1)
      (Sum.inr i) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      ∂ₜ (fun t => (vectorPotential 𝓕.c A t (space x)).ofLp i) ((time 𝓕.c) x))e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val]e_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    ((1 / 𝓕.c.val) •
        ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1)
      (Sum.inr i) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      ∂ₜ (fun t => (vectorPotential 𝓕.c A t (space x)).ofLp i) ((time 𝓕.c) x))e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val
  simp [vectorPotential, timeSlice]e_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    (𝓕.c.val⁻¹ *
      ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1
        (Sum.inr i)) =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    ((electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
      ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, space x)) (Sum.inr i)) ((time 𝓕.c) x))e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val
  ring_nfe_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1
      (Sum.inr i) =
  𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ * (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, space x)) (Sum.inr i)) ((time 𝓕.c) x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val
  congre_a.e_f.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))) ((toTimeAndSpace 𝓕.c) x).1 (Sum.inr i) =
  ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, space x)) (Sum.inr i)) ((time 𝓕.c) x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val
  rw [← Time.deriv_lorentzVectore_a.e_f.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2)) (Sum.inr i)) ((toTimeAndSpace 𝓕.c) x).1 =
  ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, space x)) (Sum.inr i)) ((time 𝓕.c) x)e_a.e_f.e_a.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.vale_a.e_f.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2)) (Sum.inr i)) ((toTimeAndSpace 𝓕.c) x).1 =
  ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, space x)) (Sum.inr i)) ((time 𝓕.c) x)e_a.e_f.e_a.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val]e_a.e_f.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2)) (Sum.inr i)) ((toTimeAndSpace 𝓕.c) x).1 =
  ∂ₜ (fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, space x)) (Sum.inr i)) ((time 𝓕.c) x)e_a.e_f.e_a.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val
  rfle_a.e_f.e_a.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2))e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x)e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val
  ·e_a.e_f.e_a.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun t => A.val ((toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2)) exact (hA.differentiable (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 2 ≠ 0 simpAll goals completed! 🐙)).comp (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun t => (toTimeAndSpace 𝓕.c).symm (t, ((toTimeAndSpace 𝓕.c) x).2) fun_propAll goals completed! 🐙)
  ·e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ fun x_1 => vectorPotential 𝓕.c A x_1 (space x) exact vectorPotential_differentiable_time A (hA.differentiable (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 2 ≠ 0 simpAll goals completed! 🐙)) x.space
  ·e_a.e_f.hfd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ Differentiable ℝ A.val exact hA.differentiable (byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ 2 ≠ 0 simpAll goals completed! 🐙)



lemma hamiltonian_eq_electricField_scalarPotential {d} {𝓕 : FreeSpace}
    (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A)
    (J : LorentzCurrentDensity d) (x : SpaceTime d) :
    A.hamiltonian 𝓕 J x =
      (1/ 𝓕.c.val^2 * 𝓕.μ₀⁻¹) * (‖A.electricField 𝓕.c (x.time 𝓕.c) x.space‖ ^ 2
      + ⟪A.electricField 𝓕.c (x.time 𝓕.c) x.space,
        Space.grad (A.scalarPotential 𝓕.c (x.time 𝓕.c) ·) x.space⟫_ℝ)
        - lagrangian 𝓕 A J x := byd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ hamiltonian 𝓕 A J x =
  1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) -
    lagrangian 𝓕 A J x
  rw [hamiltonian_eq_electricField_vectorPotential A hA J xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
      ∑ i,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
    lagrangian 𝓕 A J x =
  1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) -
    lagrangian 𝓕 A J xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
      ∑ i,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
    lagrangian 𝓕 A J x =
  1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) -
    lagrangian 𝓕 A J x]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
      ∑ i,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
          (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i -
    lagrangian 𝓕 A J x =
  1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) -
    lagrangian 𝓕 A J x
  congr 1e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) *
    ∑ i,
      (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
        (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i =
  1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
    (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
      ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
        Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ)
  conv_lhs =>
    enter [2, 2, i]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d| (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
  (∂ₜ (fun x_1 => vectorPotential 𝓕.c A x_1 (space x)) ((time 𝓕.c) x)).ofLp i
    rw [time_deriv_vectorPotential_eq_electricField]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d| (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
  (-electricField 𝓕.c A ((time 𝓕.c) x) (space x) - Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp i
  simp [mul_sub, Finset.sum_sub_distrib]e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 +
    (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp x_1 =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
      ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
        Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ)
  rw [EuclideanSpace.norm_sq_eqe_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 +
    (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp x_1 =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    (∑ i, ‖(electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i‖ ^ 2 +
      ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
        Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ)e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 +
    (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp x_1 =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    (∑ i, ‖(electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i‖ ^ 2 +
      ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
        Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ)]e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 +
    (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp x_1 =
  (𝓕.c.val ^ 2)⁻¹ * 𝓕.μ₀⁻¹ *
    (∑ i, ‖(electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i‖ ^ 2 +
      ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
        Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ)
  ring_nfe_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ * ∑ x_1, (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 ^ 2 +
    𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ *
      ∑ x_1,
        (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp x_1 =
  𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ * ∑ x_1, ‖(electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1‖ ^ 2 +
    𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ *
      ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
        Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ
  congr 1e_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ * ∑ x_1, (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 ^ 2 =
  𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ * ∑ x_1, ‖(electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1‖ ^ 2e_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ *
    ∑ x_1,
      (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
        (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp x_1 =
  𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ *
    ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
      Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ
  ·e_a.e_ad:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ * ∑ x_1, (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 ^ 2 =
  𝓕.c.val⁻¹ ^ 2 * 𝓕.μ₀⁻¹ * ∑ x_1, ‖(electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1‖ ^ 2 simpAll goals completed! 🐙
  congre_a.e_a.e_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ (fun x_1 =>
    (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
      (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp x_1) =
  fun i =>
  ⟪(electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i,
    (Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)).ofLp i⟫_ℝ
  funext ie_a.e_a.e_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp i =
  ⟪(electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i,
    (Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)).ofLp i⟫_ℝ
  simp only [RCLike.inner_apply, conj_trivial]e_a.e_a.e_a.e_fd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime di:Fin d⊢ (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i *
    (Space.grad (scalarPotential 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp i =
  (Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)).ofLp i *
    (electricField 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp i
  ringAll goals completed! 🐙

B.2. The hamiltonian in terms of the electric and magnetic fields



lemma hamiltonian_eq_electricField_magneticField (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) (x : SpaceTime d) :
    A.hamiltonian 𝓕 J x = 1/2 * 𝓕.ε₀ * (‖A.electricField 𝓕.c (x.time 𝓕.c) x.space‖ ^ 2
      + 𝓕.c ^ 2 / 2 * ∑ i, ∑ j, ‖A.magneticFieldMatrix 𝓕.c (x.time 𝓕.c) x.space (i, j)‖ ^ 2)
      + 𝓕.ε₀ * ⟪A.electricField 𝓕.c (x.time 𝓕.c) x.space,
        Space.grad (A.scalarPotential 𝓕.c (x.time 𝓕.c) ·) x.space⟫_ℝ
      + 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⊢ hamiltonian 𝓕 A J x =
  1 / 2 * 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            𝓕.c.val ^ 2 / 2 * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) +
        𝓕.ε₀ *
          ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
            Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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 [hamiltonian_eq_electricField_scalarPotential A hA J xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) -
    lagrangian 𝓕 A J x =
  1 / 2 * 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            𝓕.c.val ^ 2 / 2 * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) +
        𝓕.ε₀ *
          ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
            Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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 dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) -
    lagrangian 𝓕 A J x =
  1 / 2 * 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            𝓕.c.val ^ 2 / 2 * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) +
        𝓕.ε₀ *
          ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
            Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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 dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) -
    lagrangian 𝓕 A J x =
  1 / 2 * 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            𝓕.c.val ^ 2 / 2 * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) +
        𝓕.ε₀ *
          ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
            Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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 [lagrangian_eq_electric_magnetic A hA J xd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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) =
  1 / 2 * 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            𝓕.c.val ^ 2 / 2 * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) +
        𝓕.ε₀ *
          ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
            Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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 dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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) =
  1 / 2 * 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            𝓕.c.val ^ 2 / 2 * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) +
        𝓕.ε₀ *
          ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
            Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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 dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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) =
  1 / 2 * 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            𝓕.c.val ^ 2 / 2 * ∑ i, ∑ j, ‖magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (i, j)‖ ^ 2) +
        𝓕.ε₀ *
          ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
            Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space 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 [FreeSpace.c_sq 𝓕]d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 𝓕.ε₀ *
      (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
        ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
          Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) -
    (2⁻¹ *
          (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 -
            𝓕.μ₀⁻¹ * 2⁻¹ * ∑ x_1, ∑ x_2, magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (x_1, x_2) ^ 2) -
        scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
          LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
      ∑ x_1,
        (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1) =
  2⁻¹ * 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹ / 2 * ∑ x_1, ∑ x_2, magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (x_1, x_2) ^ 2) +
        𝓕.ε₀ *
          ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
            Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ +
      scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
    ∑ x_1,
      (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
        (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1
  field_simpd:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.valJ:LorentzCurrentDensity dx:SpaceTime d⊢ 𝓕.ε₀ *
          (‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 +
            ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
              Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ) *
        2 ^ 2 *
      𝓕.μ₀ -
    (𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 * 2 * 𝓕.μ₀ -
          ∑ x_1, ∑ x_2, magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (x_1, x_2) ^ 2 -
        2 ^ 2 * 𝓕.μ₀ * scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
          LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) +
      2 ^ 2 * 𝓕.μ₀ *
        ∑ x_1,
          (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
            (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1) =
  𝓕.ε₀ * ‖electricField 𝓕.c A ((time 𝓕.c) x) (space x)‖ ^ 2 * 2 * 𝓕.μ₀ +
          ∑ x_1, ∑ x_2, magneticFieldMatrix 𝓕.c A ((time 𝓕.c) x) (space x) (x_1, x_2) ^ 2 +
        𝓕.ε₀ *
              ⟪electricField 𝓕.c A ((time 𝓕.c) x) (space x),
                Space.grad (fun x_1 => scalarPotential 𝓕.c A ((time 𝓕.c) x) x_1) (space x)⟫_ℝ *
            2 ^ 2 *
          𝓕.μ₀ +
      2 ^ 2 * 𝓕.μ₀ * scalarPotential 𝓕.c A ((time 𝓕.c) x) (space x) *
        LorentzCurrentDensity.chargeDensity 𝓕.c J ((time 𝓕.c) x) (space x) -
    2 ^ 2 * 𝓕.μ₀ *
      ∑ x_1,
        (vectorPotential 𝓕.c A ((time 𝓕.c) x) (space x)).ofLp x_1 *
          (LorentzCurrentDensity.currentDensity 𝓕.c J ((time 𝓕.c) x) (space x)).ofLp x_1
  ringAll goals completed! 🐙