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
• C. Derivatives of tensors
  • C.1. Derivatives of tensors for 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.differentiable_vector {d : ℕ} (f : SpaceTime d → Lorentz.Vector d) : (∀ (ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun (x : SpaceTime d) => f x ν) ↔ Differentiable ℝ f

theorem SpaceTime.contDiff_vector {n : WithTop ℕ∞} {d : ℕ} (f : SpaceTime d → Lorentz.Vector d) : (∀ (ν : Fin 1 ⊕ Fin d), ContDiff ℝ n fun (x : SpaceTime d) => f x ν) ↔ ContDiff ℝ n f

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 μ)

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

@[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)

theorem SpaceTime.deriv_equivariant {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] [(realLorentzTensor d).Tensorial c M] [T2Space M] (f : SpaceTime d → M) (Λ : ↑(LorentzGroup d)) (x : SpaceTime d) (hf : Differentiable ℝ f) (μ : Fin 1 ⊕ Fin 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 μ)

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) ε = -f ((SchwartzMap.evalCLM (Lorentz.Vector.basis μ)) ((SchwartzMap.fderivCLM ℝ) ε))

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

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

C. Derivatives of tensors

Given a function f : SpaceTime d → M where M is a tensor space, we can define the derivative of f as a tensor. In particular this is ∂_μ f viewed as a tensor in Lorentz.CoVector d ⊗[ℝ] M.

def SpaceTime.tensorDeriv {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : SpaceTime d → M) : SpaceTime d → TensorProduct ℝ (Lorentz.CoVector d) M

The derivative of a tensor, as a tensor.

Equations

• SpaceTime.tensorDeriv f x = ∑ μ : Fin 1 ⊕ Fin d, Lorentz.CoVector.basis μ ⊗ₜ[ℝ] SpaceTime.deriv μ f x

theorem SpaceTime.tensorDeriv_equivariant {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] [(realLorentzTensor d).Tensorial c M] [T2Space M] (f : SpaceTime d → M) (Λ : ↑(LorentzGroup d)) (x : SpaceTime d) (hf : Differentiable ℝ f) : tensorDeriv (fun (x : SpaceTime d) => Λ • f (Λ⁻¹ • x)) x = Λ • tensorDeriv f (Λ⁻¹ • x)

theorem SpaceTime.tensorDeriv_toTensor_basis_repr {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] [(realLorentzTensor d).Tensorial c M] [T2Space M] {f : SpaceTime d → M} (hf : Differentiable ℝ f) (x : SpaceTime d) (b : TensorSpecies.Tensor.ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)) : ((TensorSpecies.Tensor.basis (Fin.append ![realLorentzTensor.Color.down] c)).repr (TensorSpecies.Tensorial.toTensor (tensorDeriv f x))) b = deriv (Lorentz.CoVector.indexEquiv (TensorSpecies.Tensor.ComponentIdx.prodEquiv b).1) (fun (x : SpaceTime d) => ((TensorSpecies.Tensor.basis c).repr (TensorSpecies.Tensorial.toTensor (f x))) (TensorSpecies.Tensor.ComponentIdx.prodEquiv b).2) x

C.1. Derivatives of tensors for distributions

def SpaceTime.distTensorDeriv {M : Type} {d : ℕ} [NormedAddCommGroup M] [InnerProductSpace ℝ M] [FiniteDimensional ℝ M] : ((SpaceTime d)→d[ℝ] M) →ₗ[ℝ] (SpaceTime d)→d[ℝ] TensorProduct ℝ (Lorentz.CoVector d) M

The derivative of a tensor, as a tensor for distributions.

Equations

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

theorem SpaceTime.distTensorDeriv_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [InnerProductSpace ℝ M] [FiniteDimensional ℝ M] (f : (SpaceTime d)→d[ℝ] M) (ε : SchwartzMap (SpaceTime d) ℝ) : (distTensorDeriv f) ε = ∑ μ : Fin 1 ⊕ Fin d, Lorentz.CoVector.basis μ ⊗ₜ[ℝ] ((distDeriv μ) f) ε

theorem SpaceTime.distTensorDeriv_equivariant {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [InnerProductSpace ℝ M] [FiniteDimensional ℝ M] [(realLorentzTensor d).Tensorial c M] (f : (SpaceTime d)→d[ℝ] M) (Λ : ↑(LorentzGroup d)) : distTensorDeriv (Λ • f) = Λ • distTensorDeriv f

theorem SpaceTime.distTensorDeriv_toTensor_basis_repr {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [InnerProductSpace ℝ M] [FiniteDimensional ℝ M] [(realLorentzTensor d).Tensorial c M] {f : (SpaceTime d)→d[ℝ] M} (ε : SchwartzMap (SpaceTime d) ℝ) (b : TensorSpecies.Tensor.ComponentIdx (Fin.append ![realLorentzTensor.Color.down] c)) : ((TensorSpecies.Tensor.basis (Fin.append ![realLorentzTensor.Color.down] c)).repr (TensorSpecies.Tensorial.toTensor ((distTensorDeriv f) ε))) b = ((TensorSpecies.Tensor.basis c).repr (TensorSpecies.Tensorial.toTensor (((distDeriv (Lorentz.CoVector.indexEquiv (TensorSpecies.Tensor.ComponentIdx.prodEquiv b).1)) f) ε))) (TensorSpecies.Tensor.ComponentIdx.prodEquiv b).2