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
• B. The Hamiltonian
  • B.1. The hamiltonian in terms of the electric and magnetic fields

iv. References

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

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 : ℕ} (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 : ℕ} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) : A.canonicalMomentum 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 : ℕ} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) : A.canonicalMomentum J = fun (x : SpaceTime d) (μ : Fin 1 ⊕ Fin d) => minkowskiMatrix μ μ • (A.fieldStrengthMatrix x) (μ, Sum.inl 0)

B. The Hamiltonian

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

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

Equations

• A.hamiltonian J x = ∑ μ : Fin 1 ⊕ Fin d, A.canonicalMomentum J x μ * SpaceTime.deriv (Sum.inl 0) A x μ - A.lagrangian J x

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

This only holds in three spatial dimensions.

theorem Electromagnetism.ElectromagneticPotential.hamiltonian_eq_electricField_magneticField (A : ElectromagneticPotential) (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity) (x : SpaceTime) : A.hamiltonian J x = 1 / 2 * (‖A.electricField (SpaceTime.time x) (SpaceTime.space x)‖ ^ 2 + ‖A.magneticField (SpaceTime.time x) (SpaceTime.space x)‖ ^ 2) + ∑ i : Fin 3, A.electricField (SpaceTime.time x) (SpaceTime.space x) i * SpaceTime.deriv (Sum.inr i) A x (Sum.inl 0) + (Lorentz.Vector.minkowskiProduct (A x)) (J x)