The vector Potential

i. Overview

The electromagnetic potential is given by A = (1/c φ, \vec A) where φ is the scalar potential and \vec A is the vector potential.

In this module we define the vector potential, and prove lemmas about it.

Since A is relativistic it is a function of SpaceTime d, whilst the vector potential is non-relativistic and is therefore a function of Time and Space d.

ii. Key results

• ElectromagneticPotential.vectorPotential : The vector potential from an electromagnetic potential.

iii. Table of contents

• A. Definition of the Vector Potential
• B. Smoothness of the vector potential
• C. Differentiablity of the vector potential

iv. References

A. Definition of the Vector Potential

noncomputable def Electromagnetism.ElectromagneticPotential.vectorPotential {d : ℕ} (c : SpeedOfLight := 1) (A : ElectromagneticPotential d) : Time → Space d → EuclideanSpace ℝ (Fin d)

The vector potential from the electromagnetic potential.

Equations

• Electromagnetism.ElectromagneticPotential.vectorPotential c A = (SpaceTime.timeSlice c) fun (x : SpaceTime d) (i : Fin d) => A x (Sum.inr i)

B. Smoothness of the vector potential

We prove various lemmas about the smoothness of the vector potential from the smoothness of the electromagnetic potential.

theorem Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff {n : WithTop ℕ∞} {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ n A) : ContDiff ℝ n ↿(vectorPotential c A)

theorem Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff {n : WithTop ℕ∞} {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ n A) (i : Fin d) : ContDiff ℝ n ↿fun (t : Time) (x : Space d) => vectorPotential c A t x i

theorem Electromagnetism.ElectromagneticPotential.vectorPotential_comp_contDiff {n : WithTop ℕ∞} {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ n A) (i : Fin d) : ContDiff ℝ n ↿fun (t : Time) (x : Space d) => vectorPotential c A t x i

theorem Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_space {n : WithTop ℕ∞} {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ n A) (t : Time) : ContDiff ℝ n (vectorPotential c A t)

theorem Electromagnetism.ElectromagneticPotential.vectorPotential_apply_contDiff_space {n : WithTop ℕ∞} {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ n A) (t : Time) (i : Fin d) : ContDiff ℝ n fun (x : Space d) => vectorPotential c A t x i

theorem Electromagnetism.ElectromagneticPotential.vectorPotential_contDiff_time {n : WithTop ℕ∞} {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ n A) (x : Space d) : ContDiff ℝ n fun (x_1 : Time) => vectorPotential c A x_1 x

C. Differentiablity of the vector potential

We prove various lemmas about the differentiablity of the vector potential from the differentiablity of the electromagnetic potential.

theorem Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) : Differentiable ℝ ↿(vectorPotential c A)

theorem Electromagnetism.ElectromagneticPotential.vectorPotential_differentiable_time {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) (x : Space d) : Differentiable ℝ fun (x_1 : Time) => vectorPotential c A x_1 x