The electromagnetic potential for distributions

i. Overview

In this file we make the basic definitions of the electromagnetic potential, the field strength tensor, the electric and magnetic fields, and the Lagrangian gradient in the context of distributions.

Note that all of these quantities depend linearly on the electromagnetic potential, allowing them to be defined in the context of distributions.

Unlike in the function case, many of the properties here can be defined as linear maps, due to the no need to check things like differentiability.

ii. Key results

• ElectromagneticPotentialD : The type of electromagnetic potentials as distributions.
• ElectromagneticPotentialD.scalarPotential : The scalar potential as a distribution.
• ElectromagneticPotentialD.vectorPotential : The vector potential as a distribution.
• ElectromagneticPotentialD.electricField : The electric field as a distribution.
• ElectromagneticPotentialD.magneticField : The magnetic field as a distribution.
• LorentzCurrentDensityD : The type of Lorentz current densities as distributions.
• ElectromagneticPotentialD.gradLagrangian : The variational gradient of the electromagnetic Lagrangian as a distribution.

iii. Table of contents

• A. The electromagnetic potential
  • A.1. The components of the electromagnetic potential
• B. The field strength tensor matrix
  • B.1. Diagonal of the field strength matrix
  • B.2. Antisymmetry of the field strength matrix
• C. The scalar and vector potentials
  • C.1. The scalar potential
  • C.2. The vector potential
• D. The electric and magnetic fields
  • D.1. Linear map to components
  • D.2. The electric field in d-dimensions
    • D.2.1. The electric field in terms of the field strength matrix
    • D.2.2. The first column of the field strength matrix in terms of the electric field
    • D.2.3. The first row of the field strength matrix in terms of the electric field
  • D.3. The magnetic field in 3-dimensions
• E. The Lorentz current density
  • E.1. The components of the Lorentz current density
• F. The Lagrangian variational gradient
  • F.1. The variational gradient in 1-dimension

iv. References

A. The electromagnetic potential

We define the electromagnetic potential as a function from spacetime to contravariant Lorentz vectors, and prove some simple results about it.

@[reducible, inline]

noncomputable abbrev Electromagnetism.ElectromagneticPotentialD (d : ℕ := 3) : Type

The electromagnetic potential is a tensor A^μ.

Equations

• Electromagnetism.ElectromagneticPotentialD d = ((SpaceTime d)→d[ℝ] Lorentz.Vector d)

A.1. The components of the electromagnetic potential

noncomputable def Electromagnetism.ElectromagneticPotentialD.toComponents {d : ℕ} : ElectromagneticPotentialD d ≃ₗ[ℝ] Fin 1 ⊕ Fin d → (SpaceTime d)→d[ℝ] ℝ

The linear map from an electromagnetic potential to its components.

Equations

• One or more equations did not get rendered due to their size.

B. The field strength tensor matrix

noncomputable def Electromagnetism.ElectromagneticPotentialD.fieldStrengthMatrix {d : ℕ} : ElectromagneticPotentialD d →ₗ[ℝ] (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) → (SpaceTime d)→d[ℝ] ℝ

The field strength matrix with indices F^μ^ν.

Equations

• One or more equations did not get rendered due to their size.

B.1. Diagonal of the field strength matrix

@[simp]

theorem Electromagnetism.ElectromagneticPotentialD.fieldStrengthMatrix_same_same {d : ℕ} (A : ElectromagneticPotentialD d) (μ : Fin 1 ⊕ Fin d) : fieldStrengthMatrix A (μ, μ) = 0

B.2. Antisymmetry of the field strength matrix

theorem Electromagnetism.ElectromagneticPotentialD.fieldStrengthMatrix_antisymm {d : ℕ} (A : ElectromagneticPotentialD d) (μ ν : Fin 1 ⊕ Fin d) : fieldStrengthMatrix A (μ, ν) = -fieldStrengthMatrix A (ν, μ)

C. The scalar and vector potentials

C.1. The scalar potential

noncomputable def Electromagnetism.ElectromagneticPotentialD.scalarPotential {d : ℕ} : ElectromagneticPotentialD d →ₗ[ℝ] (Time × Space d)→d[ℝ] ℝ

The scalar potential from an electromagnetic potential which is a distribution.

Equations

• One or more equations did not get rendered due to their size.

C.2. The vector potential

noncomputable def Electromagnetism.ElectromagneticPotentialD.vectorPotential {d : ℕ} : ElectromagneticPotentialD d →ₗ[ℝ] (Time × Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)

The vector potential from an electromagnetic potential which is a distribution.

Equations

• One or more equations did not get rendered due to their size.

D. The electric and magnetic fields

D.1. Linear map to components

noncomputable def Electromagnetism.ElectromagneticPotentialD.toComponentsEuclidean {d : ℕ} : ((Time × Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) ≃ₗ[ℝ] Fin d → (Time × Space d)→d[ℝ] ℝ

The linear map taking a distribution on Euclidean space to its components.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Electromagnetism.ElectromagneticPotentialD.toComponentsEuclidean_apply {d : ℕ} (E : (Time × Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)) (i : Fin d) (ε : SchwartzMap (Time × Space d) ℝ) : (toComponentsEuclidean E i) ε = E ε i

D.2. The electric field in d-dimensions

noncomputable def Electromagnetism.ElectromagneticPotentialD.electricField {d : ℕ} : ElectromagneticPotentialD d →ₗ[ℝ] (Time × Space d)→d[ℝ] EuclideanSpace ℝ (Fin d)

The electric field associated with a electromagnetic potential which is a distribution.

Equations

• One or more equations did not get rendered due to their size.

D.2.1. The electric field in terms of the field strength matrix

theorem Electromagnetism.ElectromagneticPotentialD.electricField_fieldStrengthMatrix {d : ℕ} {A : ElectromagneticPotentialD d} (i : Fin d) : toComponentsEuclidean (electricField A) i = SpaceTime.timeSliceD (fieldStrengthMatrix A (Sum.inr i, Sum.inl 0))

D.2.2. The first column of the field strength matrix in terms of the electric field

theorem Electromagnetism.ElectromagneticPotentialD.fieldStrengthMatrix_col_eq_electricField {d : ℕ} {A : ElectromagneticPotentialD d} (i : Fin d) : fieldStrengthMatrix A (Sum.inr i, Sum.inl 0) = SpaceTime.timeSliceD.symm (toComponentsEuclidean (electricField A) i)

D.2.3. The first row of the field strength matrix in terms of the electric field

theorem Electromagnetism.ElectromagneticPotentialD.fieldStrengthMatrix_row_eq_electricField {d : ℕ} {A : ElectromagneticPotentialD d} (i : Fin d) : fieldStrengthMatrix A (Sum.inl 0, Sum.inr i) = -SpaceTime.timeSliceD.symm (toComponentsEuclidean (electricField A) i)

D.3. The magnetic field in 3-dimensions

noncomputable def Electromagnetism.ElectromagneticPotentialD.magneticField : ElectromagneticPotentialD →ₗ[ℝ] (Time × Space)→d[ℝ] EuclideanSpace ℝ (Fin 3)

The magnetic field associated with a electromagnetic potential in 3 dimensions.

Equations

• One or more equations did not get rendered due to their size.

E. The Lorentz current density

@[reducible, inline]

abbrev Electromagnetism.LorentzCurrentDensityD (d : ℕ := 3) : Type

The Lorentz current density (aka four-current) as a distribution.

Equations

• Electromagnetism.LorentzCurrentDensityD d = ((SpaceTime d)→d[ℝ] Lorentz.Vector d)

E.1. The components of the Lorentz current density

noncomputable def Electromagnetism.LorentzCurrentDensityD.toComponents {d : ℕ} : LorentzCurrentDensityD d ≃ₗ[ℝ] Fin 1 ⊕ Fin d → (SpaceTime d)→d[ℝ] ℝ

The linear map taking a Lorentz current density to its components.

Equations

• One or more equations did not get rendered due to their size.

F. The Lagrangian variational gradient

The variational gradient of the Lagrangian density with respect to the electromagnetic potential which is a distribution. We do not prove this is correct, the proof is done for the function case.

We take the definition to be:

∑ ν, (η ν ν • (∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν)
  • Lorentz.Vector.basis ν)

which matches the result of the calculation from the function case.

noncomputable def Electromagnetism.ElectromagneticPotentialD.gradLagrangian {d : ℕ} (A : ElectromagneticPotentialD d) (J : LorentzCurrentDensityD d) : Fin 1 ⊕ Fin d → (SpaceTime d)→d[ℝ] ℝ

The variational gradient of the lagrangian for an electromagnetic potential which is a distribution. This is defined nor proved for distributions.

Equations

• One or more equations did not get rendered due to their size.

F.1. The variational gradient in 1-dimension

We simplify the variational gradient in 1-dimension.

theorem Electromagnetism.ElectromagneticPotentialD.gradLagrangian_one_dimension_electricField (A : ElectromagneticPotentialD 1) (J : LorentzCurrentDensityD 1) : A.gradLagrangian J = fun (μ : Fin 1 ⊕ Fin 1) => match μ with | Sum.inl 0 => SpaceTime.timeSliceD.symm (Space.spaceDivD (electricField A)) - LorentzCurrentDensityD.toComponents J (Sum.inl 0) | Sum.inr 0 => LorentzCurrentDensityD.toComponents J (Sum.inr 0) + SpaceTime.timeSliceD.symm (toComponentsEuclidean (Space.timeDerivD (electricField A)) 0)