The Scalar 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 scalar potential, and prove lemmas about it.

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

ii. Key results

• ElectromagneticPotential.scalarPotential : The scalar potential from an electromagnetic potential.

iii. Table of contents

• A. Definition of the Scalar Potential
• B. Smoothness of the Scalar Potential
• C. Differentiability of the Scalar Potential

iv. References

A. Definition of the Scalar Potential

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

The scalar potential from the electromagnetic potential.

Equations

• Electromagnetism.ElectromagneticPotential.scalarPotential c A = (SpaceTime.timeSlice c) fun (x : SpaceTime d) => c.val * A x (Sum.inl 0)

B. Smoothness of the Scalar Potential

We prove various lemmas about the smoothness of the scalar potential.

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

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

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

C. Differentiability of the Scalar Potential

We prove various lemmas about the differentiability of the scalar potential.

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

theorem Electromagnetism.ElectromagneticPotential.scalarPotential_differentiable_space {d : ℕ} (c : SpeedOfLight) (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) (t : Time) : Differentiable ℝ (scalarPotential c A t)

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