The constant electric and magnetic fields

i. Overview

In this module we define the electromagnetic potential which gives rise to a given constant electric and magnetic field in 3d.

We show that the kinetic term for this potential has a variational gradient equal to zero, i.e. it satisfies the source-free Maxwell equations.

ii. Key results

• ElectromagneticPotential.constantEB E₀ B₀ : An electromagnetic potential which gives rise to a given constant electric field E₀ and magnetic field B₀ in 3d.
• ElectromagneticPotential.constantEB_gradKineticTerm : The variational gradient of the kinetic term for the potential constantEB E₀ B₀ is equal to zero.

iii. Table of contents

• A. The definition of the potential
• B. Smoothness of the potential
• C. The scalar potential
• D. The vector potential
• E. The electric field
• F. The magnetic field
• G. The kinetic term
• H. The variational gradient of the kinetic term

iv. References

A. The definition of the potential

The potential which gives rise to a constant electric field E₀ and magnetic field B₀ in 3d is given by (- ⟪E₀, x⟫, (1/2) B₀ × x) where x is the spatial position vector.

noncomputable def Electromagnetism.ElectromagneticPotential.constantEB (E₀ B₀ : EuclideanSpace ℝ (Fin 3)) : ElectromagneticPotential

An electric potential in 3d which gives a given constant E-field and B-field.

Equations

• One or more equations did not get rendered due to their size.
• Electromagnetism.ElectromagneticPotential.constantEB E₀ B₀ x (Sum.inl val) = -inner ℝ E₀ (SpaceTime.space x)

B. Smoothness of the potential

The potential constantEB E₀ B₀ is smooth.

theorem Electromagnetism.ElectromagneticPotential.constantEB_smooth {E₀ B₀ : EuclideanSpace ℝ (Fin 3)} : ContDiff ℝ (↑⊤) (constantEB E₀ B₀)

C. The scalar potential

The scalar potential for constantEB E₀ B₀ is given by -⟪E₀, x⟫.

theorem Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential {E₀ B₀ : EuclideanSpace ℝ (Fin 3)} : (constantEB E₀ B₀).scalarPotential = fun (x : Time) (x : EuclideanSpace ℝ (Fin 3)) => -inner ℝ E₀ x

D. The vector potential

The vector potential for constantEB E₀ B₀ is given by (1/2) B₀ × x.

theorem Electromagnetism.ElectromagneticPotential.constantEB_vectorPotential {E₀ B₀ : EuclideanSpace ℝ (Fin 3)} : (constantEB E₀ B₀).vectorPotential = fun (x : Time) (x : WithLp 2 (Fin 3 → ℝ)) => (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) ((1 / 2) • B₀) x

E. The electric field

The electric field for constantEB E₀ B₀ is given by E₀.

@[simp]

theorem Electromagnetism.ElectromagneticPotential.constantEB_electricField {E₀ B₀ : EuclideanSpace ℝ (Fin 3)} : (constantEB E₀ B₀).electricField = fun (x : Time) (x : Space) => E₀

F. The magnetic field

The magnetic field for constantEB E₀ B₀ is given by B₀.

@[simp]

theorem Electromagnetism.ElectromagneticPotential.constantEB_magneticField {E₀ B₀ : EuclideanSpace ℝ (Fin 3)} : (constantEB E₀ B₀).magneticField = fun (x : Time) (x : Space) => B₀

G. The kinetic term

The kinetic term for constantEB E₀ B₀ is given by 1/2 (‖E₀‖² - ‖B₀‖²). Note this is not the same as the kinetic energy.

theorem Electromagnetism.ElectromagneticPotential.constantEB_kineticTerm {E₀ B₀ : EuclideanSpace ℝ (Fin 3)} (x : SpaceTime) : (constantEB E₀ B₀).kineticTerm x = 1 / 2 * (‖E₀‖ ^ 2 - ‖B₀‖ ^ 2)

H. The variational gradient of the kinetic term

The variational gradient of the kinetic term for constantEB E₀ B₀ is equal to zero.

theorem Electromagnetism.ElectromagneticPotential.constantEB_gradKineticTerm {E₀ B₀ : EuclideanSpace ℝ (Fin 3)} : (constantEB E₀ B₀).gradKineticTerm = 0