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

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 {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) : SpaceTime d → ℝ

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 {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (Λ : ↑(LorentzGroup d)) (hf : Differentiable ℝ A) (x : SpaceTime d) : kineticTerm 𝓕 (fun (x : SpaceTime d) => Λ • A (Λ⁻¹ • x)) x = kineticTerm 𝓕 A (Λ⁻¹ • x)

A.2. Kinetic term simplified expressions

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) : kineticTerm 𝓕 A x = -1 / (4 * 𝓕.μ₀) * ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, ∑ μ' : Fin 1 ⊕ Fin d, ∑ ν' : Fin 1 ⊕ Fin d, 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_fieldStrengthMatrix {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) : kineticTerm 𝓕 A x = -1 / (4 * 𝓕.μ₀) * ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, ∑ μ' : Fin 1 ⊕ Fin d, ∑ ν' : Fin 1 ⊕ Fin d, minkowskiMatrix μ μ' * minkowskiMatrix ν ν' * (A.fieldStrengthMatrix x) (μ, ν) * (A.fieldStrengthMatrix x) (μ', ν')

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_fieldStrengthMatrix_sq {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) : kineticTerm 𝓕 A x = -1 / (4 * 𝓕.μ₀) * ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, minkowskiMatrix μ μ * minkowskiMatrix ν ν * ‖(A.fieldStrengthMatrix x) (μ, ν)‖ ^ 2

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) : kineticTerm 𝓕 A x = -1 / (2 * 𝓕.μ₀) * ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, (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 {𝓕 : FreeSpace} (A : ElectromagneticPotential) (t : Time) (x : Space) (hA : Differentiable ℝ A) : kineticTerm 𝓕 A ((SpaceTime.toTimeAndSpace 𝓕.c).symm (t, x)) = 1 / 2 * (𝓕.ε₀ * ‖electricField 𝓕.c A t x‖ ^ 2 - 1 / 𝓕.μ₀ * ‖magneticField 𝓕.c A t x‖ ^ 2)

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electric_magnetic' {𝓕 : FreeSpace} {A : ElectromagneticPotential} (hA : Differentiable ℝ A) (x : SpaceTime) : kineticTerm 𝓕 A x = 1 / 2 * (𝓕.ε₀ * ‖electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)‖ ^ 2 - 1 / 𝓕.μ₀ * ‖magneticField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)‖ ^ 2)

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

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (t : Time) (x : Space d) (hA : Differentiable ℝ A) : kineticTerm 𝓕 A ((SpaceTime.toTimeAndSpace 𝓕.c).symm (t, x)) = 1 / 2 * (𝓕.ε₀ * ‖electricField 𝓕.c A t x‖ ^ 2 - 1 / (2 * 𝓕.μ₀) * ∑ i : Fin d, ∑ j : Fin d, ‖magneticFieldMatrix 𝓕.c A t x (i, j)‖ ^ 2)

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_eq_electricMatrix_magneticFieldMatrix {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) (hA : Differentiable ℝ A) : kineticTerm 𝓕 A x = 1 / 2 * (𝓕.ε₀ * ‖electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)‖ ^ 2 - 1 / (2 * 𝓕.μ₀) * ∑ i : Fin d, ∑ j : Fin d, ‖magneticFieldMatrix 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) (i, j)‖ ^ 2)

A.5. The kinetic term for constant fields

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_const {d : ℕ} {𝓕 : FreeSpace} (A₀ : Lorentz.Vector d) : (kineticTerm 𝓕 fun (x : SpaceTime d) => A₀) = 0

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_add_const {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (A₀ : Lorentz.Vector d) : (kineticTerm 𝓕 fun (x : SpaceTime d) => A x + A₀) = kineticTerm 𝓕 A

A.6. Smoothness of the kinetic term

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_contDiff {d : ℕ} {n : WithTop ℕ∞} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (n + 1) A) : ContDiff ℝ n (kineticTerm 𝓕 A)

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

This result is used in finding the canonical momentum.

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_add_time_mul_const {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (ha : Differentiable ℝ A) (c : Lorentz.Vector d) (x : SpaceTime d) : kineticTerm 𝓕 (fun (x : SpaceTime d) => A x + x (Sum.inl 0) • c) x = kineticTerm 𝓕 A x + (-1 / (2 * 𝓕.μ₀) * ∑ ν : Fin 1 ⊕ Fin d, (2 * c ν * minkowskiMatrix ν ν * SpaceTime.deriv (Sum.inl 0) A x ν + minkowskiMatrix ν ν * c ν ^ 2 - 2 * c ν * SpaceTime.deriv ν A x (Sum.inl 0)) + 1 / (2 * 𝓕.μ₀) * c (Sum.inl 0) ^ 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.gradKineticTerm {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) : SpaceTime d → Lorentz.Vector d

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

Equations

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

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 {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) : have F' := fun (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) (ψ : SpaceTime d → ℝ) (x : SpaceTime d) => -(fderiv ℝ (fun (x' : SpaceTime d) => (fun (x' : SpaceTime d) => 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 d) => SpaceTime.deriv μν.1 A x' μν.2 * (fun (x' : SpaceTime d) => minkowskiMatrix μν.1 μν.1 * minkowskiMatrix μν.2 μν.2 * ψ x') x') x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(-(fderiv ℝ (fun (x' : SpaceTime d) => ψ x' * SpaceTime.deriv μν.2 A x' μν.1) x) (Lorentz.Vector.basis μν.1) • Lorentz.Vector.basis μν.2 + -(fderiv ℝ (fun (x' : SpaceTime d) => SpaceTime.deriv μν.1 A x' μν.2 * ψ x') x) (Lorentz.Vector.basis μν.2) • Lorentz.Vector.basis μν.1); gradKineticTerm 𝓕 A = fun (x : SpaceTime d) => ∑ μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d), F' μν (fun (x' : SpaceTime d) => -1 / (2 * 𝓕.μ₀) * (fun (x : SpaceTime d) => 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 {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) (ha : ContDiff ℝ (↑⊤) A) : gradKineticTerm 𝓕 A x = ∑ ν : Fin 1 ⊕ Fin d, ∑ μ : Fin 1 ⊕ Fin d, (1 / 𝓕.μ₀ * (minkowskiMatrix μ μ * minkowskiMatrix ν ν * SpaceTime.deriv μ (fun (x' : SpaceTime d) => SpaceTime.deriv μ A x' ν) x - SpaceTime.deriv μ (fun (x' : SpaceTime d) => 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 {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) (ha : ContDiff ℝ (↑⊤) A) : gradKineticTerm 𝓕 A x = ∑ ν : Fin 1 ⊕ Fin d, (1 / 𝓕.μ₀ * minkowskiMatrix ν ν) • (∑ μ : Fin 1 ⊕ Fin d, SpaceTime.deriv μ (fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) (μ, ν)) x) • Lorentz.Vector.basis ν

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.

theorem Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) (ha : ContDiff ℝ (↑⊤) A) : gradKineticTerm 𝓕 A x = (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x)) (SpaceTime.space x)) • Lorentz.Vector.basis (Sum.inl 0) + ∑ i : Fin d, (𝓕.μ₀⁻¹ * (1 / 𝓕.c.val ^ 2 * Time.deriv (fun (t : Time) => electricField 𝓕.c A t (SpaceTime.space x)) ((SpaceTime.time 𝓕.c) x) i - ∑ j : Fin d, Space.deriv j (fun (x_1 : Space d) => magneticFieldMatrix 𝓕.c A ((SpaceTime.time 𝓕.c) x) x_1 (j, i)) (SpaceTime.space x))) • Lorentz.Vector.basis (Sum.inr i)

theorem Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three {𝓕 : FreeSpace} (A : ElectromagneticPotential) (x : SpaceTime) (ha : ContDiff ℝ (↑⊤) A) : gradKineticTerm 𝓕 A x = (1 / (𝓕.μ₀ * 𝓕.c.val) * Space.div (electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x)) (SpaceTime.space x)) • Lorentz.Vector.basis (Sum.inl 0) + ∑ i : Fin 3, (𝓕.μ₀⁻¹ * (1 / 𝓕.c.val ^ 2 * Time.deriv (fun (t : Time) => electricField 𝓕.c A t (SpaceTime.space x)) ((SpaceTime.time 𝓕.c) x) i - Space.curl (magneticField 𝓕.c A ((SpaceTime.time 𝓕.c) x)) (SpaceTime.space x) i)) • Lorentz.Vector.basis (Sum.inr i)

B.5. Linearity properties of the variational gradient

theorem Electromagnetism.ElectromagneticPotential.gradKineticTerm_add {d : ℕ} {𝓕 : FreeSpace} (A1 A2 : ElectromagneticPotential d) (hA1 : ContDiff ℝ (↑⊤) A1) (hA2 : ContDiff ℝ (↑⊤) A2) : gradKineticTerm 𝓕 (A1 + A2) = gradKineticTerm 𝓕 A1 + gradKineticTerm 𝓕 A2

theorem Electromagnetism.ElectromagneticPotential.gradKineticTerm_smul {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) (c : ℝ) : gradKineticTerm 𝓕 (c • A) = c • gradKineticTerm 𝓕 A

B.6. HasVarGradientAt for the variational gradient

theorem Electromagnetism.ElectromagneticPotential.kineticTerm_hasVarGradientAt {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (↑⊤) A) : HasVarGradientAt (kineticTerm 𝓕) (gradKineticTerm 𝓕 A) A