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.SpaceAndTime.SpaceTime.TimeSliceThe 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
DistLorentzCurrentDensity : The type of Lorentz current densities
as distributions.
iii. Table of contents
A. The Lorentz current density as a distribution
A.1. The underlying charge density
A.2. The underlying current density
iv. References
@[expose] public sectionattribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_oneA. The Lorentz current density as a distribution
The Lorentz current density, also called four-current as a distribution.
abbrev DistLorentzCurrentDensity (d : ℕ := 3) := (SpaceTime d) →d[ℝ] Lorentz.Vector d