Distributions

i. Overview of distributions

Distributions are often used implicitly in physics, for example the correct way to handle a dirac delta function is to treat it as a distribution. In this file we will define distributions and some properties on them.

The distributions from a space E to space F can be thought of as a generalization of functions from E to F. We give a more precise definition of distributions below.

ii. Key results

• E →d[𝕜] F is the type of distributions from E to F.
• Distribution.derivative and Distribution.fourierTransform allow us to make sense of these operations that might not make sense a priori on general functions.

iii. Table of Content

• A. The definition of a distribution
• B. Construction of distributions from linear maps
• C. Derivatives of distributions
• D. Fourier transform of distributions
• E. Specific distributions

iv. Implementation notes

• In this file we will define distributions generally, in PhysLean.SpaceAndTime.Distributions we define properties of distributions directly related to Space.

A. The definition of a distribution

In physics, we often encounter mathematical objects like the Dirac delta function δ(x) that are not functions in the traditional sense. Distributions provide a rigorous framework for handling such objects.

The core idea is to define a "generalized function" not by its value at each point, but by how it acts on a set of well-behaved "test functions".

These test functions, typically denoted η. The choice of test functions depends on the application here we choose test functions which are smooth and decay rapidly at infinity (called Schwartz maps). Thus really the distributions we are defining here are called tempered distributions.

A distribution u is a linear map that takes a test function η and produces a value, which can be a scalar or a vector. This action is written as ⟪u,η⟫.

Two key examples illustrate this concept:

1. Ordinary Functions: Any well-behaved function f(x) can be viewed as a distribution. Its action on a test function η is defined by integration: u_f(η) = ∫ f(x) η(x) dx This integral "tests" the function f using η.

2. Dirac Delta: The Dirac delta δ_a (centered at a) is a distribution whose action is to simply evaluate the test function at a: δ_a(η) = η(a)

Formally, a distribution is a continuous linear map from the space of Schwartz functions 𝓢(E, 𝕜) to a vector space F over 𝕜. This definition allows us to rigorously define concepts like derivatives and Fourier transforms for these generalized functions, as we will see below.

We use the notation E →d[𝕜] F to denote the space of distributions from E to F where E is a normed vector space over ℝ and F is a normed vector space over 𝕜.

@[reducible, inline]

abbrev Distribution (𝕜 E F : Type) [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace 𝕜 F] : Type

An F-valued distribution on E (where E is a normed vector space over ℝ and F is a normed vector space over 𝕜) is a continuous linear map 𝓢(E, 𝕜) →L[𝕜] F where 𝒮(E, 𝕜) is the Schwartz space of smooth functions E → 𝕜 with rapidly decreasing iterated derivatives. This is notated as E →d[𝕜] F.

This should be seen as a generalisation of functions E → F.

Equations

• (E→d[𝕜] F) = (SchwartzMap E 𝕜 →L[𝕜] F)

def «term_→d[_]_» : Lean.TrailingParserDescr

An F-valued distribution on E (where E is a normed vector space over ℝ and F is a normed vector space over 𝕜) is a continuous linear map 𝓢(E, 𝕜) →L[𝕜] F where 𝒮(E, 𝕜) is the Schwartz space of smooth functions E → 𝕜 with rapidly decreasing iterated derivatives. This is notated as E →d[𝕜] F.

This should be seen as a generalisation of functions E → F.

Equations

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

B. Construction of distributions from linear maps

Distributions are defined as continuous linear maps from 𝓢(E, 𝕜) to F. It is possible to define a constructor of distributions from just linear maps 𝓢(E, 𝕜) →ₗ[𝕜] F (without the continuity requirement) by imposing a condition on the size of u applied to η.

def Distribution.ofLinear (𝕜 : Type) {E F : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace 𝕜 F] (s : Finset (ℕ × ℕ)) (u : SchwartzMap E 𝕜 →ₗ[𝕜] F) (hu : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (η : SchwartzMap E 𝕜), ∃ (k : ℕ) (n : ℕ) (x : E), (k, n) ∈ s ∧ ‖u η‖ ≤ C * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑η) x‖)) : E→d[𝕜] F

The construction of a distribution from the following data:

1. We take a finite set s of pairs (k, n) ∈ ℕ × ℕ that will be explained later.
2. We take a linear map u that evaluates the given Schwartz function η. At this stage we don't need u to be continuous.
3. Recall that a Schwartz function η satisfies a bound ‖x‖ᵏ * ‖(dⁿ/dxⁿ) η‖ < Mₙₖ where Mₙₖ : ℝ only depends on (k, n) : ℕ × ℕ.
4. This step is where s is used: for each test function η, the norm ‖u η‖ is required to be bounded by C * (‖x‖ᵏ * ‖(dⁿ/dxⁿ) η‖) for some x : ℝ and for some (k, n) ∈ s, where C ≥ 0 is a global scalar.

Equations

• Distribution.ofLinear 𝕜 s u hu = SchwartzMap.mkCLMtoNormedSpace ⇑u ⋯ ⋯ ⋯

@[simp]

theorem Distribution.ofLinear_apply (𝕜 : Type) {E F : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace 𝕜 F] (s : Finset (ℕ × ℕ)) (u : SchwartzMap E 𝕜 →ₗ[𝕜] F) (hu : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (η : SchwartzMap E 𝕜), ∃ (k : ℕ) (n : ℕ) (x : E), (k, n) ∈ s ∧ ‖u η‖ ≤ C * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑η) x‖)) (η : SchwartzMap E 𝕜) : (ofLinear 𝕜 s u hu) η = u η

C. Derivatives of distributions

Given a distribution u : E →d[𝕜] F, we can define the derivative of that distribution. In general when defining an operation on a distribution, we do it by applying a similar operation instead to the Schwartz maps it acts on.

Thus the derivative of u is the distribution which takes η to ⟪u, - η'⟫ where η' is the derivative of η.

def Distribution.fderivD (𝕜 : Type) {E F : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [FiniteDimensional ℝ E] : (E→d[𝕜] F) →ₗ[𝕜] E→d[𝕜] E →L[ℝ] F

The Fréchet derivative of a distribution.

Informally, for a distribution u : E →d[𝕜] F, the Fréchet derivative fderiv u x v corresponds to the derivative of u at the point x in the direction v. For example, if F = ℝ³ then fderiv u x v is a vector in ℝ³ corresponding to (v₁ ∂u₁/∂x₁ + v₂ ∂u₁/∂x₂ + v₃ ∂u₁/∂x₃, v₁ ∂u₂/∂x₁ + v₂ ∂u₂/∂x₂ + v₃ ∂u₂/∂x₃,...).

Formally, for a distribution u : E →d[𝕜] F, this is actually defined the distribution which takes test function η : E → 𝕜 to - u (SchwartzMap.evalCLM v (SchwartzMap.fderivCLM 𝕜 η)).

Note that, unlike for functions, the Fréchet derivative of a distribution always exists.

Equations

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

theorem Distribution.fderivD_apply (𝕜 : Type) {E F : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [FiniteDimensional ℝ E] (u : E→d[𝕜] F) (η : SchwartzMap E 𝕜) (v : E) : (((fderivD 𝕜) u) η) v = -u ((SchwartzMap.evalCLM v) ((SchwartzMap.fderivCLM 𝕜) η))

D. Fourier transform of distributions

As with derivatives of distributions we can define the fourier transform of a distribution by taking the fourier transform of the underlying Schwartz maps. Thus the fourier transform of the distribution u is the distribution which takes η to ⟪u, F[η]⟫ where F[η] is the fourier transform of η.

def Distribution.fourierTransform (E F : Type) [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] : (E→d[ℂ] F) →ₗ[ℂ] E→d[ℂ] F

Definition of Fourier transform of distribution: Let u be a distribution. Then its Fourier transform is F{u} where given a test function η, F{u}(η) := u(F{η}).

Equations

• Distribution.fourierTransform E F = { toFun := fun (u : E→d[ℂ] F) => ContinuousLinearMap.comp u (SchwartzMap.fourierTransformCLM ℂ), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Distribution.fourierTransform_apply {E F : Type} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℂ F] (u : E→d[ℂ] F) (η : SchwartzMap E ℂ) : ((fourierTransform E F) u) η = u ((SchwartzMap.fourierTransformCLM ℂ) η)

E. Specific distributions

We now define specific distributions, which are used throughout physics. In particular, we define:

• The constant distribution.
• The dirac delta distribution.
• The heaviside step function.

E.1. The constant distribution

The constant distribution is the distribution which corresponds to a constant function, it takes η to the integral of η over the volume measure.

def Distribution.const (𝕜 : Type) {F : Type} [RCLike 𝕜] [NormedAddCommGroup F] (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [hμ : MeasureTheory.volume.HasTemperateGrowth] (c : F) : E→d[𝕜] F

The constant distribution E →d[𝕜] F, for a given c : F this corresponds to the integral ∫ x, η x • c ∂MeasureTheory.volume.

Equations

• Distribution.const 𝕜 E c = SchwartzMap.mkCLMtoNormedSpace (fun (η : SchwartzMap E 𝕜) => ∫ (x : E), η x • c) ⋯ ⋯ ⋯

theorem Distribution.const_apply (𝕜 : Type) {F : Type} [RCLike 𝕜] [NormedAddCommGroup F] (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [hμ : MeasureTheory.volume.HasTemperateGrowth] (c : F) (η : SchwartzMap E 𝕜) : (const 𝕜 E c) η = ∫ (x : E), η x • c

@[simp]

theorem Distribution.fderivD_const {E F : Type} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [MeasureTheory.MeasureSpace E] [BorelSpace E] [SecondCountableTopology E] [hμ : MeasureTheory.volume.IsAddHaarMeasure] [FiniteDimensional ℝ E] (c : F) : (fderivD ℝ) (const ℝ E c) = 0

E.2. The dirac delta distribution

The dirac delta distribution centered at a : E is the distribution which takes η to η a. We also define diracDelta' which takes in an element of v of F and outputs η a • v.

def Distribution.diracDelta (𝕜 : Type) {E : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] (a : E) : E→d[𝕜] 𝕜

Dirac delta distribution diracDelta 𝕜 a : E →d[𝕜] 𝕜 takes in a test function η : 𝓢(E, 𝕜) and outputs η a. Intuitively this is an infinite density at a single point a.

Equations

• Distribution.diracDelta 𝕜 a = SchwartzMap.delta 𝕜 𝕜 a

@[simp]

theorem Distribution.diracDelta_apply (𝕜 : Type) {E : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] (a : E) (η : SchwartzMap E 𝕜) : (diracDelta 𝕜 a) η = η a

def Distribution.diracDelta' (𝕜 : Type) {E F : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace 𝕜 F] (a : E) (v : F) : E→d[𝕜] F

Dirac delta in a given direction v : F. diracDelta' 𝕜 a v takes in a test function η : 𝓢(E, 𝕜) and outputs η a • v. Intuitively this is an infinitely intense vector field at a single point a pointing at the direction v.

Equations

• Distribution.diracDelta' 𝕜 a v = ContinuousLinearMap.smulRight (Distribution.diracDelta 𝕜 a) v

@[simp]

theorem Distribution.diracDelta'_apply (𝕜 : Type) {E F : Type} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace 𝕜 F] (a : E) (v : F) (η : SchwartzMap E 𝕜) : (diracDelta' 𝕜 a v) η = η a • v

E.3. The heviside step function

The heaviside step function on EuclideanSpace ℝ (Fin d.succ) is the distribution from EuclideanSpace ℝ (Fin d.succ) to ℝ which takes a η to the integral of η in the upper-half plane (determined by the last coordinate in EuclideanSpace ℝ (Fin d.succ)).

def Distribution.heavisideStep (d : ℕ) : (EuclideanSpace ℝ (Fin d.succ))→d[ℝ] ℝ

The Heaviside step distribution defined on (EuclideanSpace ℝ (Fin d.succ)) equal to 1 in the positive z-direction and 0 in the negative z-direction.

Equations

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

theorem Distribution.heavisideStep_apply (d : ℕ) (η : SchwartzMap (EuclideanSpace ℝ (Fin d.succ)) ℝ) : (heavisideStep d) η = ∫ (x : EuclideanSpace ℝ (Fin d.succ)) in {x : EuclideanSpace ℝ (Fin d.succ) | 0 < x (Fin.last d)}, η x