Physlib.Electromagnetism.Dynamics.CurrentDensity — Physlib

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.TimeSlice

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

              @[expose] public sectionattribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_one

A. The Lorentz Current Density

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

The Lorentz current density, also called four-current.

abbrev LorentzCurrentDensity (d : ℕ := 3) := SpaceTime d → Lorentz.Vector d

B. The underlying charge

lemma chargeDensity_eq_timeSlice {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d} :
    J.chargeDensity c = timeSlice c (fun x => (1 / (c : ℝ)) • J x (Sum.inl 0)) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity d⊢ chargeDensity c J = (timeSlice c) fun x => (1 / c.val) • J x (Sum.inl 0) rflAll goals completed! 🐙

B.1. Charge density of zero Lorentz current density

@[simp]
lemma chargeDensity_zero {d : ℕ} {c : SpeedOfLight}:
    chargeDensity c (0 : LorentzCurrentDensity d) = 0 := byd:ℕc:SpeedOfLight⊢ chargeDensity c 0 = 0
  simp [chargeDensity_eq_timeSlice, timeSlice]d:ℕc:SpeedOfLight⊢ Function.curry ((fun x => 0) ∘ ⇑(toTimeAndSpace c).symm) = 0
  rflAll goals completed! 🐙

B.2. Differentiability of the charge density



lemma chargeDensity_differentiable {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d}
    (hJ : Differentiable ℝ J) : Differentiable ℝ ↿(J.chargeDensity c) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿(chargeDensity c J)
  rw [chargeDensity_eq_timeSliced:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿((timeSlice c) fun x => (1 / c.val) • J x (Sum.inl 0))d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿((timeSlice c) fun x => (1 / c.val) • J x (Sum.inl 0))]d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿((timeSlice c) fun x => (1 / c.val) • J x (Sum.inl 0))
  apply timeSlice_differentiabled:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ fun x => (1 / c.val) • J x (Sum.inl 0)
  have h1 : ∀ i, Differentiable ℝ (fun x => J x i) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿(chargeDensity c J)d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => (1 / c.val) • J x (Sum.inl 0)
    rw [SpaceTime.differentiable_vectord:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ Jd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ Jd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => (1 / c.val) • J x (Sum.inl 0)]d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ Jd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => (1 / c.val) • J x (Sum.inl 0)
    exact hJd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => (1 / c.val) • J x (Sum.inl 0)d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => (1 / c.val) • J x (Sum.inl 0)
  apply Differentiable.fun_const_smuld:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun i => J i (Sum.inl 0)
  exact h1 (Sum.inl 0)All goals completed! 🐙

lemma chargeDensity_differentiable_space {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d}
    (hJ : Differentiable ℝ J) (t : Time) :
    Differentiable ℝ (fun x => J.chargeDensity c t x) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ fun x => chargeDensity c J t x
  change Differentiable ℝ (↿(J.chargeDensity c) ∘ fun x => (t, x))d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ (↿(chargeDensity c J) ∘ fun x => (t, x))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ ↿(chargeDensity c J)refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ fun x => (t, x)
  ·refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ ↿(chargeDensity c J) exact chargeDensity_differentiable hJAll goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ fun x => (t, x) fun_propAll goals completed! 🐙

B.3. Smoothness of the charge density



lemma chargeDensity_contDiff {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d}
    (hJ : ContDiff ℝ n J) : ContDiff ℝ n ↿(J.chargeDensity c) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿(chargeDensity c J)
  rw [chargeDensity_eq_timeSlicen:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿((timeSlice c) fun x => (1 / c.val) • J x (Sum.inl 0))n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿((timeSlice c) fun x => (1 / c.val) • J x (Sum.inl 0))]n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿((timeSlice c) fun x => (1 / c.val) • J x (Sum.inl 0))
  apply timeSlice_contDiffn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n fun x => (1 / c.val) • J x (Sum.inl 0)
  have h1 : ∀ i, ContDiff ℝ n (fun x => J x i) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿(chargeDensity c J)n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => (1 / c.val) • J x (Sum.inl 0)
    rw [SpaceTime.contDiff_vectorn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n Jn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n Jn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => (1 / c.val) • J x (Sum.inl 0)]n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n Jn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => (1 / c.val) • J x (Sum.inl 0)
    exact hJn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => (1 / c.val) • J x (Sum.inl 0)n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => (1 / c.val) • J x (Sum.inl 0)
  apply ContDiff.const_smuln:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun y => J y (Sum.inl 0)
  exact h1 (Sum.inl 0)All goals completed! 🐙

C. The underlying current density

lemma currentDensity_eq_timeSlice {d : ℕ} {J : LorentzCurrentDensity d} :
    J.currentDensity c = timeSlice c (fun x => WithLp.toLp 2
      fun i => J x (Sum.inr i)) := byc:SpeedOfLightd:ℕJ:LorentzCurrentDensity d⊢ currentDensity c J = (timeSlice c) fun x => WithLp.toLp 2 fun i => J x (Sum.inr i) rflAll goals completed! 🐙

C.1. current density of zero Lorentz current density

@[simp]
lemma currentDensity_zero {d : ℕ} {c : SpeedOfLight}:
    currentDensity c (0 : LorentzCurrentDensity d) = 0 := byd:ℕc:SpeedOfLight⊢ currentDensity c 0 = 0
  simp [currentDensity_eq_timeSlice, timeSlice]d:ℕc:SpeedOfLight⊢ Function.curry ((fun x => WithLp.toLp 2 fun i => 0) ∘ ⇑(toTimeAndSpace c).symm) = 0
  rflAll goals completed! 🐙

C.2. Differentiability of the current density

              

lemma currentDensity_differentiable {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d}
    (hJ : Differentiable ℝ J) : Differentiable ℝ ↿(J.currentDensity c) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿(currentDensity c J)
  rw [currentDensity_eq_timeSliced:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿((timeSlice c) fun x => WithLp.toLp 2 fun i => J x (Sum.inr i))d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿((timeSlice c) fun x => WithLp.toLp 2 fun i => J x (Sum.inr i))]d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿((timeSlice c) fun x => WithLp.toLp 2 fun i => J x (Sum.inr i))
  apply timeSlice_differentiabled:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)
  have h1 : ∀ i, Differentiable ℝ (fun x => J x i) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ ↿(currentDensity c J)d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)
    rw [SpaceTime.differentiable_vectord:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ Jd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ Jd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)]d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ J⊢ Differentiable ℝ Jd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)
    exact hJd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jh1:∀ (i : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => J x i⊢ Differentiable ℝ fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)
  exact differentiable_euclidean.mpr fun i => h1 (Sum.inr i)All goals completed! 🐙lemma currentDensity_apply_differentiable {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d}
    (hJ : Differentiable ℝ J) (i : Fin d) :
    Differentiable ℝ ↿(fun t x => J.currentDensity c t x i) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Ji:Fin d⊢ Differentiable ℝ ↿fun t x => (currentDensity c J t x).ofLp i
  change Differentiable ℝ (EuclideanSpace.proj i ∘ ↿(J.currentDensity c))d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Ji:Fin d⊢ Differentiable ℝ (⇑(EuclideanSpace.proj i) ∘ ↿(currentDensity c J))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Ji:Fin d⊢ Differentiable ℝ ⇑(EuclideanSpace.proj i)refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Ji:Fin d⊢ Differentiable ℝ ↿(currentDensity c J)
  ·refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Ji:Fin d⊢ Differentiable ℝ ⇑(EuclideanSpace.proj i) exact ContinuousLinearMap.differentiable (𝕜 := ℝ) (EuclideanSpace.proj i)All goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Ji:Fin d⊢ Differentiable ℝ ↿(currentDensity c J) exact currentDensity_differentiable hJAll goals completed! 🐙lemma currentDensity_differentiable_space {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d}
    (hJ : Differentiable ℝ J) (t : Time) :
    Differentiable ℝ (fun x => J.currentDensity c t x) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ fun x => currentDensity c J t x
  change Differentiable ℝ (↿(J.currentDensity c) ∘ fun x => (t, x))d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ (↿(currentDensity c J) ∘ fun x => (t, x))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ ↿(currentDensity c J)refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ fun x => (t, x)
  ·refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ ↿(currentDensity c J) exact currentDensity_differentiable hJAll goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Time⊢ Differentiable ℝ fun x => (t, x) fun_propAll goals completed! 🐙lemma currentDensity_apply_differentiable_space {d : ℕ} {c : SpeedOfLight}
    {J : LorentzCurrentDensity d}
    (hJ : Differentiable ℝ J) (t : Time) (i : Fin d) :
    Differentiable ℝ (fun x => J.currentDensity c t x i) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ fun x => (currentDensity c J t x).ofLp i
  change Differentiable ℝ (EuclideanSpace.proj i ∘ (↿(J.currentDensity c) ∘ fun x => (t, x)))d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ (⇑(EuclideanSpace.proj i) ∘ ↿(currentDensity c J) ∘ fun x => (t, x))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ ⇑(EuclideanSpace.proj i)refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ (↿(currentDensity c J) ∘ fun x => (t, x))
  ·refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ ⇑(EuclideanSpace.proj i) exact ContinuousLinearMap.differentiable (𝕜 := ℝ) _All goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ (↿(currentDensity c J) ∘ fun x => (t, x)) apply Differentiable.comp ?_ ?_d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ ↿(currentDensity c J)d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ fun x => (t, x)
    ·d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ ↿(currentDensity c J) exact currentDensity_differentiable hJAll goals completed! 🐙
    ·d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jt:Timei:Fin d⊢ Differentiable ℝ fun x => (t, x) fun_propAll goals completed! 🐙lemma currentDensity_differentiable_time {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d}
    (hJ : Differentiable ℝ J) (x : Space d) :
    Differentiable ℝ (fun t => J.currentDensity c t x) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space d⊢ Differentiable ℝ fun t => currentDensity c J t x
  change Differentiable ℝ (↿(J.currentDensity c) ∘ fun t => (t, x))d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space d⊢ Differentiable ℝ (↿(currentDensity c J) ∘ fun t => (t, x))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space d⊢ Differentiable ℝ ↿(currentDensity c J)refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space d⊢ Differentiable ℝ fun t => (t, x)
  ·refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space d⊢ Differentiable ℝ ↿(currentDensity c J) exact currentDensity_differentiable hJAll goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space d⊢ Differentiable ℝ fun t => (t, x) fun_propAll goals completed! 🐙lemma currentDensity_apply_differentiable_time {d : ℕ} {c : SpeedOfLight}
    {J : LorentzCurrentDensity d}
    (hJ : Differentiable ℝ J) (x : Space d) (i : Fin d) :
    Differentiable ℝ (fun t => J.currentDensity c t x i) := byd:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ fun t => (currentDensity c J t x).ofLp i
  change Differentiable ℝ (EuclideanSpace.proj i ∘ (↿(J.currentDensity c) ∘ fun t => (t, x)))d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ (⇑(EuclideanSpace.proj i) ∘ ↿(currentDensity c J) ∘ fun t => (t, x))
  refine Differentiable.comp ?_ ?_refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ ⇑(EuclideanSpace.proj i)refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ (↿(currentDensity c J) ∘ fun t => (t, x))
  ·refine_1d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ ⇑(EuclideanSpace.proj i) exact ContinuousLinearMap.differentiable (𝕜 := ℝ) _All goals completed! 🐙
  ·refine_2d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ (↿(currentDensity c J) ∘ fun t => (t, x)) apply Differentiable.comp ?_ ?_d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ ↿(currentDensity c J)d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ fun t => (t, x)
    ·d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ ↿(currentDensity c J) exact currentDensity_differentiable hJAll goals completed! 🐙
    ·d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:Differentiable ℝ Jx:Space di:Fin d⊢ Differentiable ℝ fun t => (t, x) fun_propAll goals completed! 🐙

C.3. Smoothness of the current density



lemma currentDensity_ContDiff {d : ℕ} {c : SpeedOfLight} {J : LorentzCurrentDensity d}
    (hJ : ContDiff ℝ n J) : ContDiff ℝ n ↿(J.currentDensity c) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿(currentDensity c J)
  rw [currentDensity_eq_timeSlicen:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿((timeSlice c) fun x => WithLp.toLp 2 fun i => J x (Sum.inr i))n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿((timeSlice c) fun x => WithLp.toLp 2 fun i => J x (Sum.inr i))]n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿((timeSlice c) fun x => WithLp.toLp 2 fun i => J x (Sum.inr i))
  apply timeSlice_contDiffn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)
  have h1 : ∀ i, ContDiff ℝ n (fun x => J x i) := byn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n ↿(currentDensity c J)n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)
    rw [SpaceTime.contDiff_vectorn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n Jn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n Jn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)]n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n J⊢ ContDiff ℝ n Jn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)
    exact hJn:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)n:WithTop ℕ∞d:ℕc:SpeedOfLightJ:LorentzCurrentDensity dhJ:ContDiff ℝ n Jh1:∀ (i : Fin 1 ⊕ Fin d), ContDiff ℝ n fun x => J x i⊢ ContDiff ℝ n fun x => WithLp.toLp 2 fun i => J x (Sum.inr i)
  exact contDiff_euclidean.mpr fun i => h1 (Sum.inr i)All goals completed! 🐙