Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Electromagnetism.Distributional.Basic
public import Mathlib.Algebra.Order.Archimedean.Real.HomThe 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 distribution of SpaceTime d, whilst
the scalar potential is non-relativistic and is therefore a distribution of Time and Space d.
ii. Key results
DistElectromagneticPotential.scalarPotential : The scalar potential from an
electromagnetic potential which is a distribution.
iii. Table of contents
A. Scalar potential for distributions
iv. References
@[expose] public sectionA. Scalar potential for distributions
attribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_one