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.

Distribution.toTemperedDistribution converts a Physlib distribution to a Mathlib tempered distribution.

Distribution.ofFiniteMeasure is the scalar distribution associated to a finite measure.

Distribution.ofFiniteMeasure_eq_iff says that finite measures are determined by their associated complex scalar distributions.

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 Physlib.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:

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 η.

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 𝕜.

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.

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 η.

The construction of a distribution from the following data:

We take a finite set s of pairs (k, n) ∈ ℕ × ℕ that will be explained later.

We take a linear map u that evaluates the given Schwartz function η. At this stage we don't need u to be continuous.

Recall that a Schwartz function η satisfies a bound ‖x‖ᵏ * ‖(dⁿ/dxⁿ) η‖ < Mₙₖ where Mₙₖ : ℝ only depends on (k, n) : ℕ × ℕ.

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.

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 η.

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.