Distributions

Let E be a real finite-dimensional normed space, Ω an open subset of E, and F a real locally convex topological vector space.

An F-valued distribution on Ω is a continuous ℝ-linear map T : 𝓓(Ω, ℝ) →L[ℝ] F, defined on the space 𝓓(Ω, ℝ) of real-valued test functions, and taking values in F. In particular, if 𝕜 is an RCLike field, 𝓓'(Ω, 𝕜) is the usual notion of real or complex distribution on Ω.

We denote the space of F-valued distributions on Ω by 𝓓'(Ω, F). Topologically, it is defined as 𝓓(Ω, ℝ) →L_c[ℝ] F, meaning that we endow it with the topology of uniform convergence on compact subsets of 𝓓(Ω, ℝ). In this particular case, this happens to coincide with the topology of 𝓓(Ω, ℝ) →L[ℝ] F, namely that of uniform convergence on bounded subsets. See the implementation notes below for more details.

Right now, this file contains very few mathematical statements. The theory will be expanded in future PRs.

Main Declarations

• 𝓓'^{n}(Ω, F) = Distribution Ω F n is the space of F-valued distributions on Ω with order at most n. See the implementation notes below for more information about the parameter n : ℕ∞; in most cases you want to use the space 𝓓'(Ω, F) = Distribution Ω F ⊤.
• Distribution.mapCLM: any continuous linear map A : F →L[ℝ] G induces a continuous linear map 𝓓'(Ω, F) →L[ℝ] 𝓓'(Ω, G). On locally integrable functions, this corresponds to applying A pointwise.

Notation

In the Distributions scope, we introduce the following notations:

• 𝓓'^{n}(Ω, F): the space of F-valued distributions on the open set Ω with order at most n : ℕ∞.
• 𝓓'(Ω, F): the space of F-valued distributions on the open set Ω, i.e 𝓓'^{⊤}(Ω, F).

Note that the parameter n here lives in ℕ∞, unlike the parameter for ContDiff which lives in WithTop ℕ∞ (to incorporate analytic functions). This means that we can't use the notation ∞ introduced for ContDiff for our regularity, because it denotes an element of WithTop ℕ∞. We could introduce another notation ∞ for ⊤ : ℕ∞, but we believe it would be confusing.

Implementation Notes

abbrev or def

At this point in time, it is not clear wether we should enforce a separation between the API for 𝓓'(Ω, F) and the more generic API about 𝓓(Ω, ℝ) →L_c[ℝ] F. For now, we have made the "default" choice to implement Distribution as an abbrev, which means that we get a lot of instances for free, but also that there is no such separation of APIs.

If this happens to be a bad decision, which will become clear while developing the theory, do not hesitate to refactor to a def instead.

Vector-valued distributions

The theory of vector-valued distributions is not as well-known as its scalar-valued analog. The definition we choose is studied in L. Schwartz, Théorie des distributions à valeurs vectorielles.

Let us give two examples of how we plan to use this level of generality:

• In the short term, this will allow us to define the Fréchet derivative of a distribution, as a continuous linear map 𝓓'(Ω, F) →L[ℝ] 𝓓'(Ω, E →L[ℝ] F). Note that, even if F = ℝ, the derivative is naturally vector-valued.
• On a longer timescale, we should aim to prove the Schwartz Kernel Theorem, which is formulated nicely in terms of vector-valued distributions. Indeed, it says precisely that one can (algebraically, at least) identify the spaces 𝓓'(Ω₁ ×ˢ Ω₂, ℝ) and 𝓓'(Ω₁, 𝓓'(Ω₂, ℝ)).

Choice of scalar field

In the literature, it is common to define complex-valued distributions as continuous ℂ-linear forms T : 𝓓(Ω, ℂ) →L[ℂ] ℂ. We use 𝓓(Ω, ℝ) →L[ℝ] ℂ instead, that is, we only ever test against real-valued test functions.

This makes no difference mathematically, since 𝓓(Ω, ℂ) is the complexification of 𝓓(Ω, ℝ), hence there is a topological isomorphism between 𝓓(Ω, ℝ) →L[ℝ] F and 𝓓(Ω, ℂ) →L[ℂ] F whenever F is a complex vector space.

We choose this definition because it avoids adding a base field as an extra parameter. Instead, we use the generality of vector-valued distributions to our advantage: a complex-valued distribution is nothing more than a distribution taking values in the real vector-space ℂ.

Order of distributions

Based on established practice in the litterature, a natural way to express the order of a distribution would be to introduce a predicate Distribution.HasOrderAtMost on the space of all distributions. Here though, we define a separate space 𝓓'^{n}(Ω, F) whose elements are precisely distributions of order at most n.

This is not incompatible with the predicate approach: in fact, we think that such a predicate should eventually become the primary interface for the order of a distribution. However, we believe that being able to talk about the space 𝓓'^{n}(Ω, F) is also quite important, for the following reasons:

• if T : 𝓓'(Ω,F) is a distribution whose order is at most n, it is natural to test it against a C^n test function (especially if n = 0). This means that we naturally want to consider its extension T' as an element of 𝓓'^{n}(Ω, F).
• it is often quite easy to keep track of the regularities while defining an operation on distributions (e. g. differentiation). On the other hand, once you have defined an operation on 𝓓'^(Ω, F), it can be quite painful to study its relation to order a posteriori.

Note that the topology on 𝓓'^{n}(Ω, F) has no reason to be the subspace topology coming from 𝓓'(Ω, F).

Choice of topology

Our choice of the compact convergence topology on 𝓓'^{n}(Ω, F) follows L. Schwartz, Théorie des distributions à valeurs vectorielles, §2, p. 49.

Note that, since 𝓓(Ω, ℝ) is a Montel space, the topology on 𝓓'(Ω, F) is also that of bounded convergence. Hence, our definition also agrees with L. Schwartz, Théorie des distributions, Chapitre III, §3.

When n is finite, however, 𝓓^{n}(Ω, ℝ) is no longer a Montel space (see L. Schwartz, Théorie des distributions, Chapitre III, §2, p. 71), hence these two topologies have no reason to be the same. Schwartz uses compact convergence as a default (see L. Schwartz, Théorie des distributions à valeurs vectorielles, §2, p. 50), which we follow here.

Finally, note that a sequence of distributions converges in 𝓓'(Ω, F) if and only if it converges pointwise (see L. Schwartz, Théorie des distributions, Chapitre III, §3, Theorème XIII). Due to this fact, some texts endow 𝓓'(Ω, F) with the pointwise convergence topology. While this gives the same converging sequences as the topology of bounded/compact convergence, this is no longer true for general filters.

References

• L. Schwartz, Théorie des distributions
• L. Schwartz, Théorie des distributions à valeurs vectorielles

@[reducible, inline]

abbrev Distribution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Ω : TopologicalSpace.Opens E) (F : Type u_2) [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (n : ℕ∞) : Type (max u_1 u_2)

𝓓'^{n}(Ω, F) = Distribution Ω F n is the space of F-valued distributions on Ω with order at most n.

In most cases you want to use the space 𝓓'(Ω, F) = Distribution Ω F ⊤.

Equations

• Distribution Ω F n = CompactConvergenceCLM (RingHom.id ℝ) (TestFunction Ω ℝ n) F

def Distributions.«term𝓓'^{_}(_,_)» : Lean.ParserDescr

We denote 𝓓'^{n}(Ω, F) the space of F-valued distributions on Ω with order at most n : ℕ∞. Note that using 𝓓' is a bit abusive since this is no longer a dual space unless F = 𝕜.

Equations

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

def Distributions.«term𝓓'(_,_)» : Lean.ParserDescr

We denote 𝓓'(Ω, F) the space of F-valued distributions on Ω. Note that using 𝓓' is a bit abusive since this is no longer a dual space unless F = 𝕜.

Equations

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

def Distribution.mapCLM {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {F' : Type u_3} [AddCommGroup F'] [Module ℝ F'] [TopologicalSpace F'] {n : ℕ∞} [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup F'] [ContinuousSMul ℝ F'] (A : F →L[ℝ] F') : Distribution Ω F n →L[ℝ] Distribution Ω F' n

Any continuous linear map A : F →L[ℝ] G induces a continuous linear map 𝓓'(Ω, F) →L[ℝ] 𝓓'(Ω, G). On locally integrable functions, this corresponds to applying A pointwise.

Equations

• Distribution.mapCLM A = ContinuousLinearMap.postcomp_uniformConvergenceCLM {S : Set (TestFunction Ω ℝ n) | IsCompact S} A

@[simp]

theorem Distribution.mapCLM_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {F' : Type u_3} [AddCommGroup F'] [Module ℝ F'] [TopologicalSpace F'] {n : ℕ∞} [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup F'] [ContinuousSMul ℝ F'] {A : F →L[ℝ] F'} {T : Distribution Ω F n} {f : TestFunction Ω ℝ n} : ((mapCLM A) T) f = A (T f)