The Lorentz Current Density

i. Overview

In this module we define the Lorentz current density and its decomposition into charge density and current density. The Lorentz current density is often called the four-current and given then the symbol J.

ii. Key results

• LorentzCurrentDensity : The type of Lorentz current densities.
• LorentzCurrentDensity.chargeDensity : The charge density associated with a Lorentz current density.
• LorentzCurrentDensity.currentDensity : The current density associated with a Lorentz current density.

iii. Table of contents

• A. The Lorentz Current Density
• B. The underlying charge density
• C. The underlying current density

iv. References

A. The Lorentz Current Density

The Lorentz current density is a Lorentz Vector field on spacetime.

@[reducible, inline]

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

The Lorentz current density, also called four-current.

Equations

• Electromagnetism.LorentzCurrentDensity d = (SpaceTime d → Lorentz.Vector d)

B. The underlying charge

noncomputable def Electromagnetism.LorentzCurrentDensity.chargeDensity {d : ℕ} (J : LorentzCurrentDensity d) : Time → Space d → ℝ

The underlying charge density associated with a Lorentz current density.

Equations

• J.chargeDensity t x = J (SpaceTime.toTimeAndSpace.symm (t, x)) (Sum.inl 0)

C. The underlying current density

noncomputable def Electromagnetism.LorentzCurrentDensity.currentDensity {d : ℕ} (J : LorentzCurrentDensity d) : Time → Space d → EuclideanSpace ℝ (Fin d)

The underlying (non-Lorentz) current density associated with a Lorentz current density.

Equations

• J.currentDensity t x i = J (SpaceTime.toTimeAndSpace.symm (t, x)) (Sum.inr i)