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

We will show that this electromagnetic potential is an extrema of the free-space electromagnetic action.

ii. Key results

iii. Table of contents

• A. The definition of the potential
• B. Smoothness of the potential
• C. The scalar potential
• D. The vector potential
  • D.1. Time derivative of the vector potential
  • D.2. Space derivative of the vector potential
• E. The electric field
• F. The magnetic field
• G. Is extrema

iv. References

A. The definition of the potential

The electromagnetic potential which gives rise to a constant electric field E₀ and a constant magnetic field matrix B₀.

noncomputable def Electromagnetism.ElectromagneticPotential.constantEB {d : ℕ} (c : SpeedOfLight) (E₀ : EuclideanSpace ℝ (Fin d)) (B₀ : Fin d × Fin d → ℝ) (B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)) : ElectromagneticPotential d

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

Equations

• Electromagnetism.ElectromagneticPotential.constantEB c E₀ B₀ B₀_antisymm x (Sum.inl val) = -(1 / c.val) * inner ℝ E₀ (SpaceTime.space x)
• Electromagnetism.ElectromagneticPotential.constantEB c E₀ B₀ B₀_antisymm x (Sum.inr i) = 1 / 2 * ∑ j : Fin d, B₀ (i, j) * SpaceTime.space x j

B. Smoothness of the potential

The potential is smooth.

theorem Electromagnetism.ElectromagneticPotential.constantEB_smooth {d : ℕ} {c : SpeedOfLight} {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ} {B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)} : ContDiff ℝ (↑⊤) (constantEB c E₀ B₀ B₀_antisymm)

C. The scalar potential

The scalar potential of the electromagnetic potential is given by -⟪E₀, x⟫.

theorem Electromagnetism.ElectromagneticPotential.constantEB_scalarPotential {d : ℕ} {c : SpeedOfLight} {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ} {B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)} : scalarPotential c (constantEB c E₀ B₀ B₀_antisymm) = fun (x : Time) (x : EuclideanSpace ℝ (Fin d)) => -inner ℝ E₀ x

D. The vector potential

The vector potential of the electromagnetic potential is (1 / 2) * ∑ j, B₀ (i, j) * x j .

theorem Electromagnetism.ElectromagneticPotential.constantEB_vectorPotential {d : ℕ} {c : SpeedOfLight} {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ} {B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)} : vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) = fun (x : Time) (x : Space d) (i : Fin d) => 1 / 2 * ∑ j : Fin d, B₀ (i, j) * x j

D.1. Time derivative of the vector potential

@[simp]

theorem Electromagnetism.ElectromagneticPotential.constantEB_vectorPotential_time_deriv {d : ℕ} {c : SpeedOfLight} {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ} {B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)} (t : Time) (x : Space d) : Time.deriv (fun (x_1 : Time) => vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) x_1 x) t = 0

D.2. Space derivative of the vector potential

theorem Electromagnetism.ElectromagneticPotential.constantEB_vectorPotential_space_deriv {d : ℕ} {c : SpeedOfLight} {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ} {B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)} (t : Time) (x : Space d) (i j : Fin d) : Space.deriv i (fun (x : Space d) => vectorPotential c (constantEB c E₀ B₀ B₀_antisymm) t x j) x = 1 / 2 * B₀ (j, i)

E. The electric field

@[simp]

theorem Electromagnetism.ElectromagneticPotential.constantEB_electricField {d : ℕ} {c : SpeedOfLight} {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ} {B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)} : electricField c (constantEB c E₀ B₀ B₀_antisymm) = fun (x : Time) (x : Space d) => E₀

F. The magnetic field

@[simp]

theorem Electromagnetism.ElectromagneticPotential.constantEB_magneticFieldMatrix {d : ℕ} {c : SpeedOfLight} {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ} {B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)} : magneticFieldMatrix c (constantEB c E₀ B₀ B₀_antisymm) = fun (x : Time) (x : Space d) => B₀

G. Is extrema

theorem Electromagnetism.ElectromagneticPotential.constantEB_isExtrema {d : ℕ} {𝓕 : FreeSpace} {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ} {B₀_antisymm : ∀ (i j : Fin d), B₀ (i, j) = -B₀ (j, i)} : IsExtrema 𝓕 (constantEB 𝓕.c E₀ B₀ B₀_antisymm) 0