Derivatives on SpaceTime

i. Overview

In this module we define and prove basic lemmas about derivatives of functions and distributions on SpaceTime d.

ii. Key results

• deriv : The derivative of a function SpaceTime d → M along the μ coordinate.
• deriv_sum_inr : The derivative along a spatial coordinate in terms of the derivative on Space d.
• deriv_sum_inl : The derivative along the temporal coordinate in terms of the derivative on Time.
• distDeriv : The derivative of a distribution on SpaceTime d along the μ coordinate.
• distDeriv_commute : Derivatives of distributions on SpaceTime d commute.

iii. Table of contents

• A. Derivatives of functions on SpaceTime d
  • A.1. The definition of the derivative
  • A.2. Basic equality lemmas
  • A.3. Derivative of the zero function
  • A.4. The derivative of a function composed with a Lorentz transformation
  • A.5. Spacetime derivatives in terms of time and space derivatives
• B. Derivatives of distributions
  • B.1. Commutation of derivatives of distributions
  • B.2. Lorentz group action on derivatives of distributions

iv. References

A. Derivatives of functions on SpaceTime d

A.1. The definition of the derivative

noncomputable def SpaceTime.deriv {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] {d : ℕ} (μ : Fin 1 ⊕ Fin d) (f : SpaceTime d → M) : SpaceTime d → M

The derivative of a function SpaceTime d → ℝ along the μ coordinate.

Equations

• SpaceTime.deriv μ f y = (fderiv ℝ f y) (Lorentz.Vector.basis μ)

def SpaceTime.«term∂_» : Lean.ParserDescr

The derivative of a function SpaceTime d → ℝ along the μ coordinate.

Equations

• SpaceTime.«term∂_» = Lean.ParserDescr.node `SpaceTime.«term∂_» 1024 (Lean.ParserDescr.symbol "∂_")

A.2. Basic equality lemmas

theorem SpaceTime.deriv_eq {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] {d : ℕ} (μ : Fin 1 ⊕ Fin d) (f : SpaceTime d → M) (y : SpaceTime d) : deriv μ f y = (fderiv ℝ f y) (Lorentz.Vector.basis μ)

theorem SpaceTime.deriv_apply_eq {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) (f : SpaceTime d → Lorentz.Vector d) (hf : Differentiable ℝ f) (y : SpaceTime d) : deriv μ f y ν = (fderiv ℝ (fun (x : SpaceTime d) => f x ν) y) (Lorentz.Vector.basis μ)

@[simp]

theorem SpaceTime.deriv_coord {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : (deriv μ fun (x : SpaceTime d) => x ν) = if μ = ν then 1 else 0

A.3. Derivative of the zero function

@[simp]

theorem SpaceTime.deriv_zero {d : ℕ} (μ : Fin 1 ⊕ Fin d) : (deriv μ fun (x : SpaceTime d) => 0) = 0

A.4. The derivative of a function composed with a Lorentz transformation

theorem SpaceTime.deriv_comp_lorentz_action {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (μ : Fin 1 ⊕ Fin d) (f : SpaceTime d → M) (hf : Differentiable ℝ f) (Λ : ↑(LorentzGroup d)) (x : SpaceTime d) : deriv μ (fun (x : SpaceTime d) => f (Λ • x)) x = ∑ ν : Fin 1 ⊕ Fin d, ↑Λ ν μ • deriv ν f (Λ • x)

A.5. Spacetime derivatives in terms of time and space derivatives

theorem SpaceTime.deriv_sum_inr {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : SpaceTime d → M) (hf : Differentiable ℝ f) (x : SpaceTime d) (i : Fin d) : deriv (Sum.inr i) f x = Space.deriv i (fun (y : Space d) => f ((toTimeAndSpace c).symm (((toTimeAndSpace c) x).1, y))) ((toTimeAndSpace c) x).2

theorem SpaceTime.deriv_sum_inl {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : SpaceTime d → M) (hf : Differentiable ℝ f) (x : SpaceTime d) : deriv (Sum.inl 0) f x = (1 / c.val) • Time.deriv (fun (t : Time) => f ((toTimeAndSpace c).symm (t, ((toTimeAndSpace c) x).2))) ((toTimeAndSpace c) x).1

B. Derivatives of distributions

noncomputable def SpaceTime.distDeriv {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin 1 ⊕ Fin d) : ((SpaceTime d)→d[ℝ] M) →ₗ[ℝ] (SpaceTime d)→d[ℝ] M

Given a distribution (function) f : Space d →d[ℝ] M the derivative of f in direction μ.

Equations

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

theorem SpaceTime.distDeriv_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin 1 ⊕ Fin d) (f : (SpaceTime d)→d[ℝ] M) (ε : SchwartzMap (SpaceTime d) ℝ) : ((distDeriv μ) f) ε = (((Distribution.fderivD ℝ) f) ε) (Lorentz.Vector.basis μ)

B.1. Commutation of derivatives of distributions

theorem SpaceTime.distDeriv_commute {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ ν : Fin 1 ⊕ Fin d) (f : (SpaceTime d)→d[ℝ] M) : (distDeriv μ) ((distDeriv ν) f) = (distDeriv ν) ((distDeriv μ) f)

B.2. Lorentz group action on derivatives of distributions

We now show how the Lorentz group action on distributions interacts with derivatives.

theorem SchwartzMap.sum_apply {α : Type} [NormedAddCommGroup α] [NormedSpace ℝ α] {ι : Type} [Fintype ι] (f : ι → SchwartzMap α ℝ) (x : α) : (∑ i : ι, f i) x = ∑ i : ι, (f i) x

theorem SpaceTime.distDeriv_comp_lorentz_action {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] [(realLorentzTensor d).Tensorial c M] [T2Space M] {μ : Fin 1 ⊕ Fin d} (Λ : ↑(LorentzGroup d)) (f : (SpaceTime d)→d[ℝ] M) : (distDeriv μ) (Λ • f) = ∑ ν : Fin 1 ⊕ Fin d, ↑Λ⁻¹ ν μ • Λ • (distDeriv ν) f