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.

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
• 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 Guass's and Ampère laws

iv. References

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

A. The kinetic term

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

noncomputable def Electromagnetism.ElectromagneticPotential.kineticTerm (A : ElectromagneticPotential) : SpaceTime → ℝ

The kinetic energy from an electromagnetic potential.

Equations

• One or more equations did not get rendered due to their size.

A.1. Lorentz invariance of the kinetic term

We show that the kinetic energy is Lorentz invariant.

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_equivariant (A : ElectromagneticPotential) (Λ : ↑(LorentzGroup 3)) (hf : Differentiable ℝ A) (x : SpaceTime) : kineticTerm (fun (x : SpaceTime) => Λ • A (Λ⁻¹ • x)) x = A.kineticTerm (Λ⁻¹ • x)

A.2. Kinetic term simplified expressions

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum (A : ElectromagneticPotential) (x : SpaceTime) : A.kineticTerm x = -1 / 4 * ∑ μ : Fin 1 ⊕ Fin 3, ∑ ν : Fin 1 ⊕ Fin 3, ∑ μ' : Fin 1 ⊕ Fin 3, ∑ ν' : Fin 1 ⊕ Fin 3, minkowskiMatrix μ μ' * minkowskiMatrix ν ν' * ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ, ν) * ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (μ', ν')

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential (A : ElectromagneticPotential) (x : SpaceTime) : A.kineticTerm x = -1 / 2 * ∑ μ : Fin 1 ⊕ Fin 3, ∑ ν : Fin 1 ⊕ Fin 3, (minkowskiMatrix μ μ * minkowskiMatrix ν ν * SpaceTime.deriv μ A x ν ^ 2 - SpaceTime.deriv μ A x ν * SpaceTime.deriv ν A x μ)

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

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic (A : ElectromagneticPotential) (t : Time) (x : Space) (hA : Differentiable ℝ A) : A.kineticTerm (SpaceTime.toTimeAndSpace.symm (t, x)) = 1 / 2 * (‖A.electricField t x‖ ^ 2 - ‖A.magneticField t x‖ ^ 2)

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.

noncomputable def Electromagnetism.ElectromagneticPotential.instInnerProductSpaceRealSpaceTimeOfNatNat_1 : InnerProductSpace ℝ SpaceTime

A local instance of an inner product structure on SpaceTime.

Equations

• Electromagnetism.ElectromagneticPotential.instInnerProductSpaceRealSpaceTimeOfNatNat_1 = SpaceTime.innerProductSpace 3

noncomputable def Electromagnetism.ElectromagneticPotential.gradKineticTerm (A : ElectromagneticPotential) : SpaceTime → Lorentz.Vector

The variational gradient of the kinetic term of an electromagnetic potential.

Equations

• A.gradKineticTerm = varGradient (fun (q' : SpaceTime → Lorentz.Vector) (x : SpaceTime) => Electromagnetism.ElectromagneticPotential.kineticTerm q' x) A

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.

theorem Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_fderiv (A : ElectromagneticPotential) (hA : ContDiff ℝ (↑⊤) A) : have F' := fun (μν : (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) (ψ : SpaceTime → ℝ) (x : SpaceTime) => -(fderiv ℝ (fun (x' : SpaceTime) => (fun (x' : SpaceTime) => minkowskiMatrix μν.1 μν.1 * minkowskiMatrix μν.2 μν.2 * ψ x') x' * SpaceTime.deriv μν.1 A x' μν.2) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun (x' : SpaceTime) => SpaceTime.deriv μν.1 A x' μν.2 * (fun (x' : SpaceTime) => minkowskiMatrix μν.1 μν.1 * minkowskiMatrix μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun (x' : SpaceTime) => ψ x' * SpaceTime.deriv μν.2 A x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun (x' : SpaceTime) => SpaceTime.deriv μν.1 A x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1); A.gradKineticTerm = fun (x : SpaceTime) => ∑ μν : (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3), F' μν (fun (x' : SpaceTime) => -1 / 2 * (fun (x : SpaceTime) => 1) x') x

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.

theorem Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_sum (A : ElectromagneticPotential) (x : SpaceTime) (ha : ContDiff ℝ (↑⊤) A) : A.gradKineticTerm x = ∑ ν : Fin 1 ⊕ Fin 3, ∑ μ : Fin 1 ⊕ Fin 3, (minkowskiMatrix μ μ * minkowskiMatrix ν ν * SpaceTime.deriv μ (fun (x' : SpaceTime) => SpaceTime.deriv μ A x' ν) x - SpaceTime.deriv μ (fun (x' : SpaceTime) => SpaceTime.deriv ν A x' μ) x) • Lorentz.Vector.basis ν

B.3. Variational gradient as a sums over fieldStrengthMatrix

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

theorem Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_fieldStrength (A : ElectromagneticPotential) (x : SpaceTime) (ha : ContDiff ℝ (↑⊤) A) : A.gradKineticTerm x = ∑ ν : Fin 1 ⊕ Fin 3, minkowskiMatrix ν ν • (∑ μ : Fin 1 ⊕ Fin 3, SpaceTime.deriv μ (fun (x : SpaceTime) => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν

B.4. Variational gradient in terms of the Guass'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.

theorem Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic (A : ElectromagneticPotential) (x : SpaceTime) (ha : ContDiff ℝ (↑⊤) A) : A.gradKineticTerm x = Space.div (A.electricField (SpaceTime.toTimeAndSpace x).1) (SpaceTime.toTimeAndSpace x).2 • Lorentz.Vector.basis (Sum.inl 0) + ∑ i : Fin 3, (Time.deriv (fun (t : Time) => A.electricField t (SpaceTime.toTimeAndSpace x).2) (SpaceTime.toTimeAndSpace x).1 i - Space.curl (A.magneticField (SpaceTime.toTimeAndSpace x).1) (SpaceTime.toTimeAndSpace x).2 i) • Lorentz.Vector.basis (Sum.inr i)