Distributions

This file defines distributions E →d[𝕜] F, which is a way to generalise functions E → F. Mathematically, a distribution u : E →d[𝕜] F takes in a test function η : E → 𝕜 that is smooth with rapidly decreasing iterated derivatives, and outputs a value in F. This operation is required to be linear and continuous. Note that the space of test functions is called the Schwartz space and is denoted 𝓢(E, 𝕜).

E is required to be a normed vector space over ℝ, and F can be a normed vector space over ℝ or ℂ (which is the field denoted 𝕜).

Important Results

• Distribution.derivative and Distribution.fourierTransform allow us to make sense of these operations that might not make sense a priori on general functions.

Examples

• Distribution.diracDelta: Dirac delta distribution at a point a : E is a distribution that takes in a test function η : 𝓢(E, 𝕜) and outputs η a.

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

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 η

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 takesn 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

def Distribution.derivative (𝕜 : Type) [RCLike 𝕜] : (ℝ→d[𝕜] 𝕜) →ₗ[𝕜] ℝ→d[𝕜] 𝕜

Definition of derivative of distribution: Let u be a distribution. Then its derivative is u' where given a test function η, u' η := -u(η'). This agrees with the distribution generated by the derivative of a differentiable function (with suitable conditions) (to be defined later), because of integral by parts (where the boundary conditions are 0 by the test functions being rapidly decreasing).

Equations

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

@[simp]

theorem Distribution.derivative_apply (𝕜 : Type) [RCLike 𝕜] (u : ℝ→d[𝕜] 𝕜) (η : SchwartzMap ℝ 𝕜) : ((derivative 𝕜) u) η = -u ((SchwartzMap.derivCLM 𝕜) η)

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 dervative of u at the point x in the direction v. For example, if F = ℝ³ then fderiv u x v is a vector in ℝ³ corrsponding 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 𝕜) η))

The constant distribution

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

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 ℂ) η)

Heaviside step function

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