Documentation

TauCeti.Analysis.Distribution.OrderZero

Distributions of order zero are Radon measures #

Let Ω be an open set of a finite-dimensional real normed space E. A linear functional T on the test functions 𝓓(Ω, ℝ) has order zero if on each compact K ⊆ Ω it is bounded in the sup norm: |T φ| ≤ C_K ‖φ‖_∞ for the test functions φ supported in K. Such a functional is the difference of two regular measures on Ω: T φ = ∫ φ dν₁ - ∫ φ dν₂, and conversely such a difference has order zero (Distribution.forall_exists_abs_le_iff_exists_regular). The measures are finite on compact subsets of Ω but need not be finite. The bound is the defining estimate of a distribution of order zero, so the theorem is stated for any linear functional on 𝓓(Ω, ℝ) (a LinearMapClass), with distributions T : 𝓓'(Ω, ℝ) as the main case; continuity is not used.

This is how a derivative of locally finite total variation becomes a measure: the distributional derivatives of a function of locally bounded variation have order zero.

The proof extends T to compactly supported continuous functions on Ω. Mollifying a continuous function with compact support in Ω by bumps of small radius gives test functions supported in a fixed compact subset of Ω that converge to it uniformly (Continuous.exists_testFunction_dist_le), and the sup-norm bound makes the values of T along such a sequence converge, to a limit independent of the sequence. The extension is a linear functional on C_c(Ω, ℝ) that is bounded on order intervals, so the Riesz–Markov–Kakutani theorem for order-bounded functionals (TauCeti.RealRMK.forall_bddAbove_image_Icc_iff_exists_regular) represents it by two regular measures.

The converse uses the sup-norm bound for integrals of test functions (TestFunction.norm_integral_le_measureReal_mul_norm).

Main results #

References #

The extension of an order-zero distribution to continuous functions #

The Radon representation #

theorem Distribution.forall_exists_abs_le_iff_exists_regular {E : Type u_1} [NormedAddCommGroup E] {Ω : TopologicalSpace.Opens E} [NormedSpace ℝ E] {𝓕 : Type u_2} [FunLike 𝓕 (TestFunction Ω ℝ ⊤) ℝ] [LinearMapClass 𝓕 ℝ (TestFunction Ω ℝ ⊤) ℝ] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (T : 𝓕) :
(∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (C : ℝ), ∀ (φ : TestFunction Ω ℝ ⊤), tsupport ⇑φ ⊆ K → |T φ| ≤ C * ‖{ toFun := ⇑φ, continuous_toFun := ⋯, map_bounded' := ⋯ }‖) ↔ ∃ (ν₁ : MeasureTheory.Measure ↥Ω) (ν₂ : MeasureTheory.Measure ↥Ω), ν₁.Regular ∧ ν₂.Regular ∧ ∀ (φ : TestFunction Ω ℝ ⊤), T φ = ∫ (x : ↥Ω), φ ↑x ∂ν₁ - ∫ (x : ↥Ω), φ ↑x ∂ν₂

A distribution of order zero is a signed Radon measure. A linear functional T on the test functions of Ω is bounded on each compact K ⊆ Ω in the sup norm, |T φ| ≤ C_K ‖φ‖_∞ for the test functions φ supported in K, if and only if there are regular measures ν₁ and ν₂ on Ω with T φ = ∫ φ dν₁ - ∫ φ dν₂ for every test function φ. The measures are finite on compact subsets of Ω but need not be finite. The bound is the defining estimate of a distribution of order zero, so T need not be assumed continuous; the main case is a distribution T : 𝓓'(Ω, ℝ).