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

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

noncomputable def Electromagnetism.ElectromagneticPotential.canonicalMomentum {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : SpaceTime d → Lorentz.Vector d

The canonical momentum associated with the lagrangian of an electromagnetic potential and a Lorentz current density.

Equations

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

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

theorem Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_gradient_kineticTerm {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) : canonicalMomentum 𝓕 A J = fun (x : SpaceTime d) => gradient (fun (v : Lorentz.Vector d) => kineticTerm 𝓕 (fun (x : SpaceTime d) => A x + x (Sum.inl 0) • v) x) 0

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

theorem Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) : canonicalMomentum 𝓕 A J = fun (x : SpaceTime d) (μ : Fin 1 ⊕ Fin d) => 1 / 𝓕.μ₀ * minkowskiMatrix μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)

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

theorem Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq_electricField {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) : canonicalMomentum 𝓕 A J = fun (x : SpaceTime d) (μ : Fin 1 ⊕ Fin d) => match μ with | Sum.inl 0 => 0 | Sum.inr i => -(1 / (𝓕.μ₀ * 𝓕.c.val)) * electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i

B. The Hamiltonian

noncomputable def Electromagnetism.ElectromagneticPotential.hamiltonian {d : ℕ} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) (x : SpaceTime d) : ℝ

The Hamiltonian associated with an electromagnetic potential and a Lorentz current density.

Equations

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

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

theorem Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_vectorPotential {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) (x : SpaceTime d) : hamiltonian 𝓕 A J x = -(1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹) * ∑ i : Fin d, electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i * Time.deriv (fun (x_1 : Time) => vectorPotential 𝓕.c A x_1 (SpaceTime.space x)) ((SpaceTime.time 𝓕.c) x) i - lagrangian 𝓕 A J x

theorem Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_scalarPotential {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) (x : SpaceTime d) : hamiltonian 𝓕 A J x = 1 / 𝓕.c.val ^ 2 * 𝓕.μ₀⁻¹ * (‖electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)‖ ^ 2 + inner ℝ (electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)) (Space.grad (fun (x_1 : Space d) => scalarPotential 𝓕.c A ((SpaceTime.time 𝓕.c) x) x_1) (SpaceTime.space x))) - lagrangian 𝓕 A J x

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

theorem Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField {d : ℕ} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) (x : SpaceTime d) : hamiltonian 𝓕 A J x = 1 / 2 * 𝓕.ε₀ * (‖electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)‖ ^ 2 + 𝓕.c.val ^ 2 / 2 * ∑ i : Fin d, ∑ j : Fin d, ‖magneticFieldMatrix 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) (i, j)‖ ^ 2) + 𝓕.ε₀ * inner ℝ (electricField 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x)) (Space.grad (fun (x_1 : Space d) => scalarPotential 𝓕.c A ((SpaceTime.time 𝓕.c) x) x_1) (SpaceTime.space x)) + scalarPotential 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) * LorentzCurrentDensity.chargeDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) - ∑ i : Fin d, vectorPotential 𝓕.c A ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i * LorentzCurrentDensity.currentDensity 𝓕.c J ((SpaceTime.time 𝓕.c) x) (SpaceTime.space x) i