Distributions on SpaceTime

i. Overview

In this module we give the basic properties of distributions on SpaceTime d, and derivatives thereof.

ii. Key results

• SpaceTime.constD d m : the constant distribution on SpaceTime d with value m.
• SpaceTime.timeSliceD : the time slice of a distribution on SpaceTime d to a distribution on Time × Space d.
• SpaceTime.derivD μ f : the derivative of a distribution f : (SpaceTime d) →d[ℝ] M in direction μ : Fin 1 ⊕ Fin d.

iii. Table of contents

• A. The constant distribution on SpaceTime
• B. The time slice of a distribution on SpaceTime
• C. Derivatives of distributions
  • C.1. Relationship between the time slice and derivatives

iv. References

A. The constant distribution on SpaceTime

noncomputable def SpaceTime.constD {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (d : ℕ) (m : M) : (SpaceTime d)→d[ℝ] M

The constant distribution from SpaceTime d to a module M associated with m : M.

Equations

• SpaceTime.constD d m = Distribution.const ℝ (SpaceTime d) m

B. The time slice of a distribution on SpaceTime

noncomputable def SpaceTime.timeSliceD {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] : ((SpaceTime d)→d[ℝ] M) ≃L[ℝ] (Time × Space d)→d[ℝ] M

The time slice of a distribution on SpaceTime d to form a distribution on Time × Space d.

Equations

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

C. Derivatives of distributions

noncomputable def SpaceTime.derivD {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.derivD_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (μ : Fin 1 ⊕ Fin d) (f : (SpaceTime d)→d[ℝ] M) (ε : SchwartzMap (SpaceTime d) ℝ) : ((derivD μ) f) ε = (((Distribution.fderivD ℝ) f) ε) (Lorentz.Vector.basis μ)

C.1. Relationship between the time slice and derivatives

theorem SpaceTime.timeSliceD_derivD_inl {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : (SpaceTime d)→d[ℝ] M) : timeSliceD ((derivD (Sum.inl 0)) f) = Space.timeDerivD (timeSliceD f)

theorem SpaceTime.timeSliceD_symm_derivD_inl {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : (Time × Space d)→d[ℝ] M) : (derivD (Sum.inl 0)) (timeSliceD.symm f) = timeSliceD.symm (Space.timeDerivD f)

theorem SpaceTime.timeSliceD_derivD_inr {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) (f : (SpaceTime d)→d[ℝ] M) : timeSliceD ((derivD (Sum.inr i)) f) = (Space.spaceDerivD i) (timeSliceD f)

theorem SpaceTime.timeSliceD_symm_derivD_inr {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (i : Fin d) (f : (Time × Space d)→d[ℝ] M) : (derivD (Sum.inr i)) (timeSliceD.symm f) = timeSliceD.symm ((Space.spaceDerivD i) f)