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 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 distribution of SpaceTime d, whilst
the vector potential is non-relativistic and is therefore a distribution of Time and Space d.
ii. Key results
DistElectromagneticPotential.vectorPotential : The vector potential from an
electromagnetic potential which is a distribution.
iii. Table of contents
A. Vector potential for distributions
iv. References
@[expose] public sectionA. Vector potential for distributions
attribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_one