1. Physlib
  2. Electromagnetism
  3. Dynamics
  4. KineticTerm
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.Kinematics.MagneticField public import Physlib.Electromagnetism.Dynamics.Basic public import Physlib.Mathematics.VariationalCalculus.HasVarGradient

The kinetic term

i. Overview

The kinetic term of the electromagnetic field is - 1/(4 μ₀) F_μν F^μν. We define this, show it is invariant under Lorentz transformations, and show properties of its variational gradient.

In particular the variational gradient gradKineticTerm of the kinetic term is directly related to Gauss's law and the Ampere law.

In this implementation we have set μ₀ = 1. It is a TODO to introduce this constant.

ii. Key results

    ElectromagneticPotential.kineticTerm is the kinetic term of an electromagnetic potential.

    ElectromagneticPotential.kineticTerm_equivariant shows that the kinetic term is Lorentz invariant.

    ElectromagneticPotential.gradKineticTerm is the variational gradient of the kinetic term.

    ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic gives a first expression for the variational gradient in terms of the electric and magnetic fields.

iii. Table of contents

    A. The kinetic term

      A.1. Lorentz invariance of the kinetic term

      A.2. Kinetic term simplified expressions

      A.3. The kinetic term in terms of the electric and magnetic fields

      A.4. The kinetic term in terms of the electric and magnetic matrix

      A.5. The kinetic term for constant fields

      A.6. Smoothness of the kinetic term

      A.7. The kinetic term shifted by time mul a constant

    B. Variational gradient of the kinetic term

      B.1. Variational gradient in terms of fderiv

      B.2. Writing the variational gradient as a sums over double derivatives of the potential

      B.3. Variational gradient as a sums over fieldStrengthMatrix

      B.4. Variational gradient in terms of the Gauss's and Ampère laws

      B.5. Linearity properties of the variational gradient

      B.6. HasVarGradientAt for the variational gradient

      B.7. Gradient of the kinetic term in terms of the tensor derivative

iv. References

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

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

A. The kinetic term

The kinetic term is - 1/(4 μ₀) F_μν F^μν. We define this and show that it is Lorentz invariant.

A.1. Lorentz invariance of the kinetic term

We show that the kinetic energy is Lorentz invariant.

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime d⊢ -1 / (4 * 𝓕.μ₀) * toField ((contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor ((Λ • A).toFieldStrength x)))))) (Tensorial.toTensor ((Λ • A).toFieldStrength x))))) = -1 / (4 * 𝓕.μ₀) * toField ((contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength (Λ⁻¹ • x))))))) (Tensorial.toTensor (A.toFieldStrength (Λ⁻¹ • x)))))) conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime d| toField ((contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor ((Λ • A).toFieldStrength x)))))) (Tensorial.toTensor ((Λ • A).toFieldStrength x))))) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime d| toField ((contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (Λ • coMetric d)) (Λ • coMetric d))) (Λ • Tensorial.toTensor (A.toFieldStrength (Λ⁻¹ • x))))))) (Λ • Tensorial.toTensor (A.toFieldStrength (Λ⁻¹ • x)))))) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime d| toField ((contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength (Λ⁻¹ • x))))))) (Tensorial.toTensor (A.toFieldStrength (Λ⁻¹ • x))))))

A.2. Kinetic term simplified expressions

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime d⊢ -1 / (4 * 𝓕.μ₀) * ∑ x_1, ((basis (Fin.append ((Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 2 5) ∘ Fin.succSuccAbove 0 3) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 1 3)).repr ((contrT 2 1 3 ⋯) ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x)))))) (Tensorial.toTensor (A.toFieldStrength x))))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (x_1, x_1)) = -1 / (4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', ∑ ν', η μ μ' * η ν ν' * ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) * ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν') conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d| ((basis (Fin.append ((Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 2 5) ∘ Fin.succSuccAbove 0 3) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 1 3)).repr ((contrT 2 1 3 ⋯) ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x)))))) (Tensorial.toTensor (A.toFieldStrength x))))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d| ∑ x_1, ((basis (Fin.append ((Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 2 5) ∘ Fin.succSuccAbove 0 3) (Fin.append ![Color.up] ![Color.up]))).repr ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x)))))) (Tensorial.toTensor (A.toFieldStrength x)))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (x_1, x_1)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ((basis (Fin.append ((Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 2 5) ∘ Fin.succSuccAbove 0 3) (Fin.append ![Color.up] ![Color.up]))).repr ((prodT ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x)))))) (Tensorial.toTensor (A.toFieldStrength x)))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ((basis ((Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 2 5) ∘ Fin.succSuccAbove 0 3)).repr ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x)))))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1 * ((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (A.toFieldStrength x))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ((basis ((Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 2 5) ∘ Fin.succSuccAbove 0 3)).repr ((contrT 2 0 3 ⋯) ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x)))))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ∑ x_1, ((basis (Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 2 5)).repr ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x))))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (x_1, x_1)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin d| ((basis (Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]) ∘ Fin.succSuccAbove 2 5)).repr ((contrT 4 2 5 ⋯) ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x))))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ')) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin d| ∑ x_1, ((basis (Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]))).repr ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x)))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (x_1, x_1)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis (Fin.append (Fin.append ![Color.down, Color.down] ![Color.down, Color.down]) (Fin.append ![Color.up] ![Color.up]))).repr ((prodT ((prodT (coMetric d)) (coMetric d))) (Tensorial.toTensor (A.toFieldStrength x)))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν')) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis (Fin.append ![Color.down, Color.down] ![Color.down, Color.down])).repr ((prodT (coMetric d)) (coMetric d))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1 * ((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (A.toFieldStrength x))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis (Fin.append ![Color.down, Color.down] ![Color.down, Color.down])).repr ((prodT (coMetric d)) (coMetric d))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis ![Color.down, Color.down]).repr (coMetric d)) (ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).1 * ((basis ![Color.down, Color.down]).repr (coMetric d)) (ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis ![Color.down, Color.down]).repr (coMetric d)) (ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).1 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis ![Color.down, Color.down]).repr (coMetric d)) (ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).1 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| η ((ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).1 0) ((ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).1 1) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| η μ' μ conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis ![Color.down, Color.down]).repr (coMetric d)) (ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis ![Color.down, Color.down]).repr (coMetric d)) (ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| η ((ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).2 0) ((ComponentIdx.prod (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).1).2 1) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| η ν' ν conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (A.toFieldStrength x))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).2 0, (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).1) (μ', μ'))) (ν', ν'))).2 1) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν') conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ((basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (A.toFieldStrength x))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).2 0, (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun j => j.elim0) (μ, μ))) (ν, ν))).2 1) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d| ∑ ν, (∑ μ', ∑ ν', η μ' μ * η ν' ν * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν')) * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| (∑ μ', ∑ ν', η μ' μ * η ν' ν * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν')) * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ∑ i, (∑ ν', η i μ * η ν' ν * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (i, ν')) * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin d| (∑ ν', η μ' μ * η ν' ν * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν')) * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin d| ∑ i, η μ' μ * η i ν * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', i) * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| η μ' μ * η ν' ν * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν') * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dμ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d| η μ' μ * η ν' ν * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν') * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d| ∑ ν, ∑ μ', ∑ ν', η μ' μ * η ν' ν * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν') * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν); d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d| ∑ y, ∑ x_1, ∑ ν', η y μ * η ν' x_1 * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (y, ν') * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, x_1) conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime d| -1 / (4 * 𝓕.μ₀) * ∑ y, ∑ x_1, ∑ x_2, ∑ ν', η y x_1 * η ν' x_2 * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (y, ν') * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (x_1, x_2) conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ':Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ∑ x_1, ∑ ν', η μ' ν * η ν' x_1 * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν') * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (ν, x_1); d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ':Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ∑ y, ∑ x_1, η μ' ν * η y x_1 * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', y) * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (ν, x_1) conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ':Fin 1 ⊕ Fin d| ∑ ν, ∑ y, ∑ x_1, η μ' ν * η y x_1 * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', y) * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (ν, x_1); d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ':Fin 1 ⊕ Fin d| ∑ y, ∑ x_1, ∑ x_2, η μ' x_1 * η y x_2 * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', y) * ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (x_1, x_2) All goals completed! 🐙All goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ η μ μ * η ν ν * (A.fieldStrengthMatrix x) (μ, ν) * (A.fieldStrengthMatrix x) (μ, ν) = η μ μ * η ν ν * ‖(A.fieldStrengthMatrix x) (μ, ν)‖ ^ 2 All goals completed! 🐙All goals completed! 🐙 _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ((η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) + (η ν ν * η μ μ * (∂_ ν A x μ) ^ 2 - ∂_ ν A x μ * ∂_ μ A x ν)) := d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime d⊢ -1 / (4 * 𝓕.μ₀) * ∑ μ, ∑ ν, η μ μ * η ν ν * (η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ) * (η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ) = -1 / (4 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ + (η ν ν * η μ μ * ∂_ ν A.val x μ ^ 2 - ∂_ ν A.val x μ * ∂_ μ A.val x ν)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime d⊢ ∑ μ, ∑ ν, η μ μ * η ν ν * (η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ) * (η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ) = ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ + (η ν ν * η μ μ * ∂_ ν A.val x μ ^ 2 - ∂_ ν A.val x μ * ∂_ μ A.val x ν)) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dx✝¹:μ ∈ Finset.univν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ η μ μ * η ν ν * (η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ) * (η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ) = η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ + (η ν ν * η μ μ * ∂_ ν A.val x μ ^ 2 - ∂_ ν A.val x μ * ∂_ μ A.val x ν) All goals completed! 🐙 _ = - 1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) := d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime d⊢ -1 / (4 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ + (η ν ν * η μ μ * ∂_ ν A.val x μ ^ 2 - ∂_ ν A.val x μ * ∂_ μ A.val x ν)) = -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime d⊢ -1 / (4 * 𝓕.μ₀) * (∑ x_1, ∑ x_2, (η x_1 x_1 * η x_2 x_2 * ∂_ x_1 A.val x x_2 ^ 2 - ∂_ x_1 A.val x x_2 * ∂_ x_2 A.val x x_1) + ∑ x_1, ∑ x_2, (η x_2 x_2 * η x_1 x_1 * ∂_ x_2 A.val x x_1 ^ 2 - ∂_ x_2 A.val x x_1 * ∂_ x_1 A.val x x_2)) = -1 / (2 * 𝓕.μ₀) * ∑ x_1, ∑ x_2, (η x_1 x_1 * η x_2 x_2 * ∂_ x_1 A.val x x_2 ^ 2 - ∂_ x_1 A.val x x_2 * ∂_ x_2 A.val x x_1) conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime d| ∑ x_1, ∑ x_2, (η x_2 x_2 * η x_1 x_1 * ∂_ x_2 A.val x x_1 ^ 2 - ∂_ x_2 A.val x x_1 * ∂_ x_1 A.val x x_2) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime d| ∑ y, ∑ x_1, (η y y * η x_1 x_1 * ∂_ y A.val x x_1 ^ 2 - ∂_ y A.val x x_1 * ∂_ x_1 A.val x y) All goals completed! 🐙

A.3. The kinetic term in terms of the electric and magnetic fields

𝓕:FreeSpaceA:ElectromagneticPotentialt:Timex:SpacehA:Differentiable ℝ (A.val 3)⊢ -((-(electricField 𝓕.c A t x).ofLp 0 ^ 2 + -(electricField 𝓕.c A t x).ofLp 1 ^ 2 + -(electricField 𝓕.c A t x).ofLp 2 ^ 2 + (-(electricField 𝓕.c A t x).ofLp 0 ^ 2 + 1 / (𝓕.ε₀ * 𝓕.μ₀) * ((magneticField 𝓕.c A t x).ofLp 2 ^ 2 + (magneticField 𝓕.c A t x).ofLp 1 ^ 2) + (-(electricField 𝓕.c A t x).ofLp 1 ^ 2 + 1 / (𝓕.ε₀ * 𝓕.μ₀) * ((magneticField 𝓕.c A t x).ofLp 2 ^ 2 + (magneticField 𝓕.c A t x).ofLp 0 ^ 2)) + (-(electricField 𝓕.c A t x).ofLp 2 ^ 2 + 1 / (𝓕.ε₀ * 𝓕.μ₀) * ((magneticField 𝓕.c A t x).ofLp 1 ^ 2 + (magneticField 𝓕.c A t x).ofLp 0 ^ 2)))) * 2) = 4 * (1 / (𝓕.ε₀ * 𝓕.μ₀)) * (𝓕.μ₀ * 𝓕.ε₀ * ((electricField 𝓕.c A t x).ofLp 0 ^ 2 + (electricField 𝓕.c A t x).ofLp 1 ^ 2 + (electricField 𝓕.c A t x).ofLp 2 ^ 2) - ((magneticField 𝓕.c A t x).ofLp 0 ^ 2 + (magneticField 𝓕.c A t x).ofLp 1 ^ 2 + (magneticField 𝓕.c A t x).ofLp 2 ^ 2)) 𝓕:FreeSpaceA:ElectromagneticPotentialt:Timex:SpacehA:Differentiable ℝ (A.val 3)⊢ -(((-(electricField 𝓕.c A t x).ofLp 0 ^ 2 + -(electricField 𝓕.c A t x).ofLp 1 ^ 2 + -(electricField 𝓕.c A t x).ofLp 2 ^ 2) * 𝓕.ε₀ * 𝓕.μ₀ + (-((electricField 𝓕.c A t x).ofLp 0 ^ 2 * 𝓕.ε₀ * 𝓕.μ₀) + ((magneticField 𝓕.c A t x).ofLp 2 ^ 2 + (magneticField 𝓕.c A t x).ofLp 1 ^ 2) + (-((electricField 𝓕.c A t x).ofLp 1 ^ 2 * 𝓕.ε₀ * 𝓕.μ₀) + ((magneticField 𝓕.c A t x).ofLp 2 ^ 2 + (magneticField 𝓕.c A t x).ofLp 0 ^ 2)) + (-((electricField 𝓕.c A t x).ofLp 2 ^ 2 * 𝓕.ε₀ * 𝓕.μ₀) + ((magneticField 𝓕.c A t x).ofLp 1 ^ 2 + (magneticField 𝓕.c A t x).ofLp 0 ^ 2)))) * 2) = 4 * (𝓕.ε₀ * 𝓕.μ₀ * ((electricField 𝓕.c A t x).ofLp 0 ^ 2 + (electricField 𝓕.c A t x).ofLp 1 ^ 2 + (electricField 𝓕.c A t x).ofLp 2 ^ 2) - ((magneticField 𝓕.c A t x).ofLp 0 ^ 2 + (magneticField 𝓕.c A t x).ofLp 1 ^ 2 + (magneticField 𝓕.c A t x).ofLp 2 ^ 2)) All goals completed! 🐙All goals completed! 🐙

A.4. The kinetic term in terms of the electric and magnetic matrix

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dt:Timex:Space dhA:Differentiable ℝ A.valh1:∑ i, ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) ^ 2 = ∑ i, ∑ j, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr i, Sum.inr j) ^ 2h2:‖electricField 𝓕.c A t x‖ ^ 2 = 𝓕.c.val ^ 2 * ∑ i, |(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr i)| ^ 2⊢ (𝓕.μ₀⁻¹ * ∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr x_1) ^ 2) * (1 / 4) + (𝓕.μ₀⁻¹ * ∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inl 0) ^ 2) * (1 / 4) + (𝓕.μ₀⁻¹ * ∑ x_1, ∑ x_2, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inr x_2) ^ 2) * (-1 / 4) = (𝓕.μ₀⁻¹ * ∑ x_1, ∑ x_2, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inr x_2) ^ 2) * (-1 / 4) + 𝓕.ε₀ * (𝓕.c.val ^ 2 * ∑ i, |(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr i)| ^ 2) * (1 / 2) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dt:Timex:Space dhA:Differentiable ℝ A.valh1:∑ i, ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) ^ 2 = ∑ i, ∑ j, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr i, Sum.inr j) ^ 2h2:‖electricField 𝓕.c A t x‖ ^ 2 = 𝓕.c.val ^ 2 * ∑ i, |(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr i)| ^ 2⊢ (𝓕.μ₀⁻¹ * ∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr x_1) ^ 2) * 4⁻¹ + (𝓕.μ₀⁻¹ * ∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inl 0) ^ 2) * 4⁻¹ + (𝓕.μ₀⁻¹ * ∑ x_1, ∑ x_2, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inr x_2) ^ 2) * (-1 / 4) = (𝓕.μ₀⁻¹ * ∑ x_1, ∑ x_2, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inr x_2) ^ 2) * (-1 / 4) + 𝓕.ε₀ * (𝓕.c.val ^ 2 * ∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr x_1) ^ 2) * 2⁻¹ conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dt:Timex:Space dhA:Differentiable ℝ A.valh1:∑ i, ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) ^ 2 = ∑ i, ∑ j, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr i, Sum.inr j) ^ 2h2:‖electricField 𝓕.c A t x‖ ^ 2 = 𝓕.c.val ^ 2 * ∑ i, |(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr i)| ^ 2i:Fin d| (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr i, Sum.inl 0) ^ 2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dt:Timex:Space dhA:Differentiable ℝ A.valh1:∑ i, ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) ^ 2 = ∑ i, ∑ j, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr i, Sum.inr j) ^ 2h2:‖electricField 𝓕.c A t x‖ ^ 2 = 𝓕.c.val ^ 2 * ∑ i, |(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr i)| ^ 2i:Fin d| (-(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr i)) ^ 2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dt:Timex:Space dhA:Differentiable ℝ A.valh1:∑ i, ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) ^ 2 = ∑ i, ∑ j, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr i, Sum.inr j) ^ 2h2:‖electricField 𝓕.c A t x‖ ^ 2 = 𝓕.c.val ^ 2 * ∑ i, |(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr i)| ^ 2⊢ (𝓕.μ₀⁻¹ * ∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr x_1) ^ 2) * 4⁻¹ + (𝓕.μ₀⁻¹ * ∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr x_1) ^ 2) * 4⁻¹ + (𝓕.μ₀⁻¹ * ∑ x_1, ∑ x_2, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inr x_2) ^ 2) * (-1 / 4) = (𝓕.μ₀⁻¹ * ∑ x_1, ∑ x_2, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inr x_2) ^ 2) * (-1 / 4) + 𝓕.ε₀ * (𝓕.μ₀⁻¹ * 𝓕.ε₀⁻¹ * ∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr x_1) ^ 2) * 2⁻¹ d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dt:Timex:Space dhA:Differentiable ℝ A.valh1:∑ i, ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) ^ 2 = ∑ i, ∑ j, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr i, Sum.inr j) ^ 2h2:‖electricField 𝓕.c A t x‖ ^ 2 = 𝓕.c.val ^ 2 * ∑ i, |(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr i)| ^ 2⊢ ((∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr x_1) ^ 2) * (1 + 1) + -∑ x_1, ∑ x_2, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inr x_2) ^ 2) * 2 = -((∑ x_1, ∑ x_2, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inr x_1, Sum.inr x_2) ^ 2) * 2) + (∑ x_1, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x))) (Sum.inl 0, Sum.inr x_1) ^ 2) * 4 All goals completed! 🐙All goals completed! 🐙

A.5. The kinetic term for constant fields

lemma kineticTerm_const {d} {𝓕 : FreeSpace} (A₀ : Lorentz.Vector d) : kineticTerm 𝓕 ⟨fun _ : SpaceTime d => A₀⟩ = 0 := d:ℕ𝓕:FreeSpaceA₀:Lorentz.Vector d⊢ kineticTerm 𝓕 { val := fun x => A₀ } = 0 d:ℕ𝓕:FreeSpaceA₀:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 { val := fun x => A₀ } x = 0 x All goals completed! 🐙lemma kineticTerm_add_const {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (A₀ : Lorentz.Vector d) : kineticTerm 𝓕 ⟨fun x => A x + A₀⟩ = kineticTerm 𝓕 A := d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dA₀:Lorentz.Vector d⊢ kineticTerm 𝓕 { val := fun x => A.val x + A₀ } = kineticTerm 𝓕 A d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dA₀:Lorentz.Vector dx:SpaceTime d⊢ kineticTerm 𝓕 { val := fun x => A.val x + A₀ } x = kineticTerm 𝓕 A x All goals completed! 🐙

A.6. Smoothness of the kinetic term

d:ℕn:ℕ∞ω𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.val⊢ ContDiff ℝ n fun x => -1 / (4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', ∑ ν', η μ μ' * η ν ν' * (A.fieldStrengthMatrix x) (μ, ν) * (A.fieldStrengthMatrix x) (μ', ν') d:ℕn:ℕ∞ω𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.valh:∀ (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)), ContDiff ℝ n fun x => (A.fieldStrengthMatrix x) μν⊢ ContDiff ℝ n fun x => -1 / (4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', ∑ ν', η μ μ' * η ν ν' * (A.fieldStrengthMatrix x) (μ, ν) * (A.fieldStrengthMatrix x) (μ', ν') All goals completed! 🐙

A.7. The kinetic term shifted by time mul a constant

This result is used in finding the canonical momentum.

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dha:Differentiable ℝ A.valc:Lorentz.Vector dx:SpaceTime ddiff_a:(∂_ (Sum.inl 0) fun x => A.val x + x (Sum.inl 0) • c) = ∂_ (Sum.inl 0) A.val + fun x => cdiff_b:∀ (i : Fin d), (∂_ (Sum.inr i) fun x => A.val x + x (Sum.inl 0) • c) = ∂_ (Sum.inr i) A.valhdiff:∀ (μ ν : Fin 1 ⊕ Fin d), ∂_ μ (fun x => A.val x + x (Sum.inl 0) • c) x ν = ∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0key:∀ (μ ν : Fin 1 ⊕ Fin d), η μ μ * η ν ν * (∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0) ^ 2 - (∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0) * (∂_ ν A.val x μ + if ν = Sum.inl 0 then c μ else 0) = η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ + (((if μ = Sum.inl 0 then 2 * (c ν * η μ μ * η ν ν * ∂_ μ A.val x ν) + η μ μ * η ν ν * c ν ^ 2 - c ν * ∂_ ν A.val x μ else 0) - if ν = Sum.inl 0 then c μ * ∂_ μ A.val x ν else 0) - (if μ = Sum.inl 0 then c ν else 0) * if ν = Sum.inl 0 then c μ else 0)⊢ -1 / (2 * 𝓕.μ₀) * ∑ x_1, ∑ x_2, (η x_1 x_1 * η x_2 x_2 * (∂_ x_1 A.val x x_2 + if x_1 = Sum.inl 0 then c x_2 else 0) ^ 2 - (∂_ x_1 A.val x x_2 + if x_1 = Sum.inl 0 then c x_2 else 0) * (∂_ x_2 A.val x x_1 + if x_2 = Sum.inl 0 then c x_1 else 0)) = -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ) + (-1 / (2 * 𝓕.μ₀) * ∑ ν, (2 * c ν * η ν ν * ∂_ (Sum.inl 0) A.val x ν + η ν ν * c ν ^ 2 - 2 * c ν * ∂_ ν A.val x (Sum.inl 0)) + 1 / (2 * 𝓕.μ₀) * c (Sum.inl 0) ^ 2) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dha:Differentiable ℝ A.valc:Lorentz.Vector dx:SpaceTime ddiff_a:(∂_ (Sum.inl 0) fun x => A.val x + x (Sum.inl 0) • c) = ∂_ (Sum.inl 0) A.val + fun x => cdiff_b:∀ (i : Fin d), (∂_ (Sum.inr i) fun x => A.val x + x (Sum.inl 0) • c) = ∂_ (Sum.inr i) A.valhdiff:∀ (μ ν : Fin 1 ⊕ Fin d), ∂_ μ (fun x => A.val x + x (Sum.inl 0) • c) x ν = ∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0key:∀ (μ ν : Fin 1 ⊕ Fin d), η μ μ * η ν ν * (∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0) ^ 2 - (∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0) * (∂_ ν A.val x μ + if ν = Sum.inl 0 then c μ else 0) = η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ + (((if μ = Sum.inl 0 then 2 * (c ν * η μ μ * η ν ν * ∂_ μ A.val x ν) + η μ μ * η ν ν * c ν ^ 2 - c ν * ∂_ ν A.val x μ else 0) - if ν = Sum.inl 0 then c μ * ∂_ μ A.val x ν else 0) - (if μ = Sum.inl 0 then c ν else 0) * if ν = Sum.inl 0 then c μ else 0)⊢ -1 / (2 * 𝓕.μ₀) * ∑ x_1, ∑ x_2, (η x_1 x_1 * η x_2 x_2 * ∂_ x_1 A.val x x_2 ^ 2 - ∂_ x_1 A.val x x_2 * ∂_ x_2 A.val x x_1 + (((if x_1 = Sum.inl 0 then 2 * (c x_2 * η x_1 x_1 * η x_2 x_2 * ∂_ x_1 A.val x x_2) + η x_1 x_1 * η x_2 x_2 * c x_2 ^ 2 - c x_2 * ∂_ x_2 A.val x x_1 else 0) - if x_2 = Sum.inl 0 then c x_1 * ∂_ x_1 A.val x x_2 else 0) - (if x_1 = Sum.inl 0 then c x_2 else 0) * if x_2 = Sum.inl 0 then c x_1 else 0)) = -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ) + (-1 / (2 * 𝓕.μ₀) * ∑ ν, (2 * c ν * η ν ν * ∂_ (Sum.inl 0) A.val x ν + η ν ν * c ν ^ 2 - 2 * c ν * ∂_ ν A.val x (Sum.inl 0)) + 1 / (2 * 𝓕.μ₀) * c (Sum.inl 0) ^ 2) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dha:Differentiable ℝ A.valc:Lorentz.Vector dx:SpaceTime ddiff_a:(∂_ (Sum.inl 0) fun x => A.val x + x (Sum.inl 0) • c) = ∂_ (Sum.inl 0) A.val + fun x => cdiff_b:∀ (i : Fin d), (∂_ (Sum.inr i) fun x => A.val x + x (Sum.inl 0) • c) = ∂_ (Sum.inr i) A.valhdiff:∀ (μ ν : Fin 1 ⊕ Fin d), ∂_ μ (fun x => A.val x + x (Sum.inl 0) • c) x ν = ∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0key:∀ (μ ν : Fin 1 ⊕ Fin d), η μ μ * η ν ν * (∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0) ^ 2 - (∂_ μ A.val x ν + if μ = Sum.inl 0 then c ν else 0) * (∂_ ν A.val x μ + if ν = Sum.inl 0 then c μ else 0) = η μ μ * η ν ν * ∂_ μ A.val x ν ^ 2 - ∂_ μ A.val x ν * ∂_ ν A.val x μ + (((if μ = Sum.inl 0 then 2 * (c ν * η μ μ * η ν ν * ∂_ μ A.val x ν) + η μ μ * η ν ν * c ν ^ 2 - c ν * ∂_ ν A.val x μ else 0) - if ν = Sum.inl 0 then c μ * ∂_ μ A.val x ν else 0) - (if μ = Sum.inl 0 then c ν else 0) * if ν = Sum.inl 0 then c μ else 0)⊢ -1 / (𝓕.μ₀ + 𝓕.μ₀) * (∑ x_1, ∑ x_2, η x_1 x_1 * η x_2 x_2 * ∂_ x_1 A.val x x_2 ^ 2 - ∑ x_1, ∑ x_2, ∂_ x_1 A.val x x_2 * ∂_ x_2 A.val x x_1) + -1 / (𝓕.μ₀ + 𝓕.μ₀) * (∑ x_1, c x_1 * η x_1 x_1 * ∂_ (Sum.inl 0) A.val x x_1 + ∑ x_1, c x_1 * η x_1 x_1 * ∂_ (Sum.inl 0) A.val x x_1 + ∑ x, η x x * c x ^ 2 - ∑ x_1, c x_1 * ∂_ x_1 A.val x (Sum.inl 0) - ∑ x_1, c x_1 * ∂_ x_1 A.val x (Sum.inl 0) - c (Sum.inl 0) * c (Sum.inl 0)) = -1 / (𝓕.μ₀ + 𝓕.μ₀) * (∑ x_1, ∑ x_2, η x_1 x_1 * η x_2 x_2 * ∂_ x_1 A.val x x_2 ^ 2 - ∑ x_1, ∑ x_2, ∂_ x_1 A.val x x_2 * ∂_ x_2 A.val x x_1) + (-1 / (𝓕.μ₀ + 𝓕.μ₀) * (∑ x_1, c x_1 * η x_1 x_1 * ∂_ (Sum.inl 0) A.val x x_1 + ∑ x_1, c x_1 * η x_1 x_1 * ∂_ (Sum.inl 0) A.val x x_1 + ∑ x, η x x * c x ^ 2 - (∑ x_1, c x_1 * ∂_ x_1 A.val x (Sum.inl 0) + ∑ x_1, c x_1 * ∂_ x_1 A.val x (Sum.inl 0))) + 1 / (𝓕.μ₀ + 𝓕.μ₀) * c (Sum.inl 0) ^ 2) All goals completed! 🐙

B. Variational gradient of the kinetic term

We define the variational gradient of the kinetic term, which is the left-hand side of Gauss's law and Ampère's law in vacuum.

B.1. Variational gradient in terms of fderiv

We give a first simplification of the variational gradient in terms of the a complicated expression involving fderiv. This is not very useful in itself, but acts as a starting point for further simplifications.

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valF:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) → SpaceTime d → ℝ := fun x A' x_1 => match x with | (μ, ν) => η μ μ * η ν ν * ∂_ μ A' x_1 ν ^ 2 - ∂_ μ A' x_1 ν * ∂_ ν A' x_1 μF_h:∀ (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)), HasVarAdjDerivAt (F μν) (fun ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) A.val⊢ HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ { val := A' }.val x ν ^ 2 - ∂_ μ { val := A' }.val x ν * ∂_ ν { val := A' }.val x μ)) (fun x => ∑ μν, (fun μν ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) μν (fun x' => -1 / (2 * 𝓕.μ₀) * (fun x => 1) x') x) A.val d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valF:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) → SpaceTime d → ℝ := fun x A' x_1 => match x with | (μ, ν) => η μ μ * η ν ν * ∂_ μ A' x_1 ν ^ 2 - ∂_ μ A' x_1 ν * ∂_ ν A' x_1 μF_h:∀ (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)), HasVarAdjDerivAt (F μν) (fun ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) A.valhF_mul:HasVarAdjDerivAt (fun φ x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) φ x) (fun ψ x => ∑ i, (-(fderiv ℝ (fun x' => (fun x' => η i.1 i.1 * η i.2 i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x' * ∂_ i.1 A.val x' i.2) x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(fderiv ℝ (fun x' => ∂_ i.1 A.val x' i.2 * (fun x' => η i.1 i.1 * η i.2 i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x') x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(-(fderiv ℝ (fun x' => (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x' * ∂_ i.2 A.val x' i.1) x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(fderiv ℝ (fun x' => ∂_ i.1 A.val x' i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x) (Lorentz.Vector.basis i.2) • Lorentz.Vector.basis i.1))) A.val⊢ HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ { val := A' }.val x ν ^ 2 - ∂_ μ { val := A' }.val x ν * ∂_ ν { val := A' }.val x μ)) (fun x => ∑ μν, (fun μν ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) μν (fun x' => -1 / (2 * 𝓕.μ₀) * (fun x => 1) x') x) A.val d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valF:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) → SpaceTime d → ℝ := fun x A' x_1 => match x with | (μ, ν) => η μ μ * η ν ν * ∂_ μ A' x_1 ν ^ 2 - ∂_ μ A' x_1 ν * ∂_ ν A' x_1 μF_h:∀ (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)), HasVarAdjDerivAt (F μν) (fun ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) A.valhF_mul:HasVarAdjDerivAt (fun φ x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) φ x) (fun ψ x => ∑ i, (-(fderiv ℝ (fun x' => (fun x' => η i.1 i.1 * η i.2 i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x' * ∂_ i.1 A.val x' i.2) x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(fderiv ℝ (fun x' => ∂_ i.1 A.val x' i.2 * (fun x' => η i.1 i.1 * η i.2 i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x') x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(-(fderiv ℝ (fun x' => (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x' * ∂_ i.2 A.val x' i.1) x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(fderiv ℝ (fun x' => ∂_ i.1 A.val x' i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x) (Lorentz.Vector.basis i.2) • Lorentz.Vector.basis i.1))) A.val⊢ HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) A' x) (fun x => ∑ μν, (fun μν ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) μν (fun x' => -1 / (2 * 𝓕.μ₀) * (fun x => 1) x') x) A.val All goals completed! 🐙

B.2. Writing the variational gradient as a sums over double derivatives of the potential

We rewrite the variational gradient as a simple double sum over second derivatives of the potential.

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dha:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (-2 * ((η μ μ * η ν ν * -1 / (2 * 𝓕.μ₀)) • fderiv ℝ (fun x' => ∂_ μ A.val x' ν) x) (Lorentz.Vector.basis μ) + 2 * ((-1 / (2 * 𝓕.μ₀)) • fderiv ℝ (fun x' => ∂_ ν A.val x' μ) x) (Lorentz.Vector.basis μ)) • Lorentz.Vector.basis ν = (1 / 𝓕.μ₀ * (η μ μ * η ν ν * ∂_ μ (fun x' => ∂_ μ A.val x' ν) x - ∂_ μ (fun x' => ∂_ ν A.val x' μ) x)) • Lorentz.Vector.basis ν d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dha:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (-(2 * (-(η μ μ * η ν ν) / (2 * 𝓕.μ₀) * (fderiv ℝ (fun x' => (fderiv ℝ A.val x') (Lorentz.Vector.basis μ) ν) x) (Lorentz.Vector.basis μ))) + 2 * (-1 / (2 * 𝓕.μ₀) * (fderiv ℝ (fun x' => (fderiv ℝ A.val x') (Lorentz.Vector.basis ν) μ) x) (Lorentz.Vector.basis μ))) • Lorentz.Vector.basis ν = (𝓕.μ₀⁻¹ * (η μ μ * η ν ν * (fderiv ℝ (fun x' => (fderiv ℝ A.val x') (Lorentz.Vector.basis μ) ν) x) (Lorentz.Vector.basis μ) - (fderiv ℝ (fun x' => (fderiv ℝ A.val x') (Lorentz.Vector.basis ν) μ) x) (Lorentz.Vector.basis μ))) • Lorentz.Vector.basis ν All goals completed! 🐙

B.3. Variational gradient as a sums over fieldStrengthMatrix

We rewrite the variational gradient as a simple double sum over the fieldStrengthMatrix.

All goals completed! 🐙

B.4. Variational gradient in terms of the Gauss's and Ampère laws

We rewrite the variational gradient in terms of the electric and magnetic fields, explicitly relating it to Gauss's law and Ampère's law.

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dha:ContDiff ℝ ∞ A.valj:Fin d⊢ -(𝓕.μ₀⁻¹ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, Sum.inr j)) x) • Lorentz.Vector.basis (Sum.inr j) = (𝓕.μ₀⁻¹ * ((𝓕.c.val ^ 2)⁻¹ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp j - (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp j + ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, Sum.inr j)) ((toTimeAndSpace 𝓕.c).symm ((time 𝓕.c) x, space x))))) • Lorentz.Vector.basis (Sum.inr j)d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dha:ContDiff ℝ ∞ A.valj:Fin d⊢ ContDiff ℝ 2 A.val d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dha:ContDiff ℝ ∞ A.valj:Fin d⊢ -(𝓕.μ₀⁻¹ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, Sum.inr j)) x) = 𝓕.μ₀⁻¹ * ((𝓕.c.val ^ 2)⁻¹ * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp j - (1 / 𝓕.c.val ^ 2 * (∂ₜ (fun t => electricField 𝓕.c A t (space x)) ((time 𝓕.c) x)).ofLp j + ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, Sum.inr j)) ((toTimeAndSpace 𝓕.c).symm ((time 𝓕.c) x, space x))))d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dha:ContDiff ℝ ∞ A.valj:Fin d⊢ ContDiff ℝ 2 A.val d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dha:ContDiff ℝ ∞ A.valj:Fin d⊢ ContDiff ℝ 2 A.val All goals completed! 🐙𝓕:FreeSpaceA:ElectromagneticPotentialx:SpaceTimeha:ContDiff ℝ ∞ (A.val 3)⊢ (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) = (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 - (curl (magneticField 𝓕.c A ((time 𝓕.c) x)) (space x)).ofLp i)) • Lorentz.Vector.basis (Sum.inr i) All goals completed! 🐙

B.5. Linearity properties of the variational gradient

d:ℕ𝓕:FreeSpaceA1:ElectromagneticPotential dA2:ElectromagneticPotential dhA1:ContDiff ℝ ∞ A1.valhA2:ContDiff ℝ ∞ A2.valx:SpaceTime dν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univμ:Fin 1 ⊕ Fin d⊢ (fderiv ℝ (fun x => (A1.fieldStrengthMatrix x) (μ, ν)) x + fderiv ℝ (fun x => (A2.fieldStrengthMatrix x) (μ, ν)) x) (Lorentz.Vector.basis μ) = (fderiv ℝ (fun x => (A1.fieldStrengthMatrix x) (μ, ν)) x) (Lorentz.Vector.basis μ) + (fderiv ℝ (fun x => (A2.fieldStrengthMatrix x) (μ, ν)) x) (Lorentz.Vector.basis μ) All goals completed! 🐙d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valc:ℝx✝²:SpaceTime dν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univx:SpaceTime d⊢ (c • A.fieldStrengthMatrix x) (μ, ν) = (c • fun x => (A.fieldStrengthMatrix x) (μ, ν)) x All goals completed! 🐙

B.6. HasVarGradientAt for the variational gradient

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valF:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) → SpaceTime d → ℝ := fun x A' x_1 => match x with | (μ, ν) => η μ μ * η ν ν * ∂_ μ A' x_1 ν ^ 2 - ∂_ μ A' x_1 ν * ∂_ ν A' x_1 μF_h:∀ (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)), HasVarAdjDerivAt (F μν) (fun ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) A.val⊢ HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ { val := A' }.val x ν ^ 2 - ∂_ μ { val := A' }.val x ν * ∂_ ν { val := A' }.val x μ)) (fun x => ∑ μν, (fun μν ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) μν (fun x' => -1 / (2 * 𝓕.μ₀) * (fun x => 1) x') x) A.val d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valF:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) → SpaceTime d → ℝ := fun x A' x_1 => match x with | (μ, ν) => η μ μ * η ν ν * ∂_ μ A' x_1 ν ^ 2 - ∂_ μ A' x_1 ν * ∂_ ν A' x_1 μF_h:∀ (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)), HasVarAdjDerivAt (F μν) (fun ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) A.valhF_mul:HasVarAdjDerivAt (fun φ x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) φ x) (fun ψ x => ∑ i, (-(fderiv ℝ (fun x' => (fun x' => η i.1 i.1 * η i.2 i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x' * ∂_ i.1 A.val x' i.2) x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(fderiv ℝ (fun x' => ∂_ i.1 A.val x' i.2 * (fun x' => η i.1 i.1 * η i.2 i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x') x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(-(fderiv ℝ (fun x' => (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x' * ∂_ i.2 A.val x' i.1) x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(fderiv ℝ (fun x' => ∂_ i.1 A.val x' i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x) (Lorentz.Vector.basis i.2) • Lorentz.Vector.basis i.1))) A.val⊢ HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, (η μ μ * η ν ν * ∂_ μ { val := A' }.val x ν ^ 2 - ∂_ μ { val := A' }.val x ν * ∂_ ν { val := A' }.val x μ)) (fun x => ∑ μν, (fun μν ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) μν (fun x' => -1 / (2 * 𝓕.μ₀) * (fun x => 1) x') x) A.val d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valF:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d → Lorentz.Vector d) → SpaceTime d → ℝ := fun x A' x_1 => match x with | (μ, ν) => η μ μ * η ν ν * ∂_ μ A' x_1 ν ^ 2 - ∂_ μ A' x_1 ν * ∂_ ν A' x_1 μF_h:∀ (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)), HasVarAdjDerivAt (F μν) (fun ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) A.valhF_mul:HasVarAdjDerivAt (fun φ x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) φ x) (fun ψ x => ∑ i, (-(fderiv ℝ (fun x' => (fun x' => η i.1 i.1 * η i.2 i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x' * ∂_ i.1 A.val x' i.2) x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(fderiv ℝ (fun x' => ∂_ i.1 A.val x' i.2 * (fun x' => η i.1 i.1 * η i.2 i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x') x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(-(fderiv ℝ (fun x' => (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x' * ∂_ i.2 A.val x' i.1) x) (Lorentz.Vector.basis i.1) • Lorentz.Vector.basis i.2 + -(fderiv ℝ (fun x' => ∂_ i.1 A.val x' i.2 * (fun x' => -1 / (2 * 𝓕.μ₀) * ψ x') x') x) (Lorentz.Vector.basis i.2) • Lorentz.Vector.basis i.1))) A.val⊢ HasVarGradientAt (fun A' x => -1 / (2 * 𝓕.μ₀) * ∑ μ, ∑ ν, F (μ, ν) A' x) (fun x => ∑ μν, (fun μν ψ x => -(fderiv ℝ (fun x' => (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x' * ∂_ μν.1 A.val x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * (fun x' => η μν.1 μν.1 * η μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun x' => ψ x' * ∂_ μν.2 A.val x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun x' => ∂_ μν.1 A.val x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1)) μν (fun x' => -1 / (2 * 𝓕.μ₀) * (fun x => 1) x') x) A.val All goals completed! 🐙

B.7. Gradient of the kinetic term in terms of the tensor derivative

d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin d⊢ gradKineticTerm 𝓕 A x ν = η ν ν * (𝓕.μ₀⁻¹ * ∑ x_1, ((Tensor.basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (x_1, x_1))) conv_rhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin d| ((Tensor.basis (Fin.append ![Color.down] (Fin.append ![Color.up] ![Color.up]))).repr (Tensorial.toTensor (tensorDeriv A.toFieldStrength x))) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ)) rw [tensorDeriv_toTensor_basis_repr (d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin d⊢ Differentiable ℝ A.toFieldStrength All goals completed! 🐙)] d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx✝:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx:SpaceTime d| ((Tensor.basis (Fin.append ![Color.up] ![Color.up])).repr (Tensorial.toTensor (A.toFieldStrength x))) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ))).2 d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx✝:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx:SpaceTime d| ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ))).2 0, (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ))).2 1) d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx✝:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin dμ:Fin 1 ⊕ Fin dx:SpaceTime d| (A.fieldStrengthMatrix x) ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ))).2 0, (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ))).2 1) conv_lhs => d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin d| (∑ ν, (1 / 𝓕.μ₀ * η ν ν) • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν) ν d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin d| 𝓕.μ₀⁻¹ * η ν ν * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x d:ℕ𝓕:FreeSpaceA:ElectromagneticPotential dx:SpaceTime dhA:ContDiff ℝ ∞ A.valν:Fin 1 ⊕ Fin d⊢ 𝓕.μ₀⁻¹ * η ν ν * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x = 𝓕.μ₀⁻¹ * η ν ν * ∑ μ, ∂_ (Lorentz.CoVector.indexEquiv (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ))).1) (fun x => (A.fieldStrengthMatrix x) ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ))).2 0, (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) (Lorentz.Vector.indexEquiv.symm ν (IsReindexing.inv id ⋯ i))) (μ, μ))).2 1)) x All goals completed! 🐙