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.

The current density is given in terms of the charge density ρ and the current density \vec j as J = (c ρ, \vec 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
  • B.1. Charge density of zero Lorentz current density
  • B.2. Differentiability of the charge density
  • B.3. Smoothness of the charge density
• C. The underlying current density
  • C.1. current density of zero Lorentz current density
  • C.2. Differentiability of the current density
  • C.3. Smoothness of the 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 : ℕ} (c : SpeedOfLight := 1) (J : LorentzCurrentDensity d) : Time → Space d → ℝ

The underlying charge density associated with a Lorentz current density.

Equations

• Electromagnetism.LorentzCurrentDensity.chargeDensity c J t x = 1 / c.val * J ((SpaceTime.toTimeAndSpace c).symm (t, x)) (Sum.inl 0)

theorem Electromagnetism.LorentzCurrentDensity.chargeDensity_eq_timeSlice {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} : chargeDensity c J = (SpaceTime.timeSlice c) fun (x : SpaceTime d) => (1 / c.val) • J x (Sum.inl 0)

B.1. Charge density of zero Lorentz current density

@[simp]

theorem Electromagnetism.LorentzCurrentDensity.chargeDensity_zero {d : ℕ} {c : SpeedOfLight} : chargeDensity c 0 = 0

B.2. Differentiability of the charge density

theorem Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : Differentiable ℝ J) : Differentiable ℝ ↿(chargeDensity c J)

theorem Electromagnetism.LorentzCurrentDensity.chargeDensity_differentiable_space {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : Differentiable ℝ J) (t : Time) : Differentiable ℝ fun (x : Space d) => chargeDensity c J t x

B.3. Smoothness of the charge density

theorem Electromagnetism.LorentzCurrentDensity.chargeDensity_contDiff {n : WithTop ℕ∞} {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : ContDiff ℝ n J) : ContDiff ℝ n ↿(chargeDensity c J)

C. The underlying current density

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

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

Equations

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

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_eq_timeSlice {c : SpeedOfLight} {d : ℕ} {J : LorentzCurrentDensity d} : currentDensity c J = (SpaceTime.timeSlice c) fun (x : SpaceTime d) (i : Fin d) => J x (Sum.inr i)

C.1. current density of zero Lorentz current density

@[simp]

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_zero {d : ℕ} {c : SpeedOfLight} : currentDensity c 0 = 0

C.2. Differentiability of the current density

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : Differentiable ℝ J) : Differentiable ℝ ↿(currentDensity c J)

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : Differentiable ℝ J) (i : Fin d) : Differentiable ℝ ↿fun (t : Time) (x : Space d) => currentDensity c J t x i

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_space {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : Differentiable ℝ J) (t : Time) : Differentiable ℝ fun (x : Space d) => currentDensity c J t x

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_space {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : Differentiable ℝ J) (t : Time) (i : Fin d) : Differentiable ℝ fun (x : Space d) => currentDensity c J t x i

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_differentiable_time {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : Differentiable ℝ J) (x : Space d) : Differentiable ℝ fun (t : Time) => currentDensity c J t x

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_apply_differentiable_time {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : Differentiable ℝ J) (x : Space d) (i : Fin d) : Differentiable ℝ fun (t : Time) => currentDensity c J t x i

C.3. Smoothness of the current density

theorem Electromagnetism.LorentzCurrentDensity.currentDensity_ContDiff {n : WithTop ℕ∞} {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} (hJ : ContDiff ℝ n J) : ContDiff ℝ n ↿(currentDensity c J)