Distributions from bounded functions

In this module we define distributions from functions f : EuclideanSpace ℝ (Fin d.succ) → F whose norm is bounded by c1 * ‖x‖ ^ (-d : ℝ) + c2 * ‖x‖ ^ n for some constants c1, c2 and n.

This gives a convenient way to construct distributions from functions, without needing to reference the underlying Schwartz maps.

Key definition

• ofBounded: Creates a distribution from a bounded function f.

Method of definition

The ofBounded function is defined through two measures invPowMeasure and powMeasure n, the first is the measure with density 1/‖x‖ᵈ and the second is the measure with density ‖x‖^n. Both these measures are proven to have temperate growth, and can be used to define a distribution by intergration.

We also define a boundMeasure which is a linear combination of these two measures.

The measures.

def Distribution.invPowMeasure {dm1 : ℕ} : MeasureTheory.Measure (EuclideanSpace ℝ (Fin dm1.succ))

The measure on EuclideanSpace ℝ (Fin 3) weighted by 1 / ‖x‖ ^ 2.

Equations

• Distribution.invPowMeasure = MeasureTheory.volume.withDensity fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => ENNReal.ofReal (1 / ‖x‖ ^ dm1)

def Distribution.powMeasure {dm1 : ℕ} (n : ℕ) : MeasureTheory.Measure (EuclideanSpace ℝ (Fin dm1.succ))

The measure on EuclideanSpace ℝ (Fin 3) weighted by ‖x‖ ^ n.

Equations

• Distribution.powMeasure n = MeasureTheory.volume.withDensity fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => ENNReal.ofReal (‖x‖ ^ n)

def Distribution.boundMeasure {dm1 : ℕ} (n : ℕ) (C1 C2 : ℝ) : MeasureTheory.Measure (EuclideanSpace ℝ (Fin dm1.succ))

The measure on EuclideanSpace ℝ (Fin 3) given by C1 • invPowMeasure + C2 • powMeasure n, for constants C1 and C2.

Equations

• Distribution.boundMeasure n C1 C2 = ENNReal.ofReal C1 • Distribution.invPowMeasure + ENNReal.ofReal C2 • Distribution.powMeasure n

Integrable conditions for the measures.

theorem Distribution.integrable_boundMeasure {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (n : ℕ) (C1 C2 : ℝ) (C1_nonneg : 0 ≤ C1) (C2_nonneg : 0 ≤ C2) (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (h : MeasureTheory.Integrable f (boundMeasure n C1 C2)) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => (C1 * (1 / ‖x‖ ^ dm1) + C2 * ‖x‖ ^ n) • f x) MeasureTheory.volume

Integrals with respect to the measures.

theorem Distribution.integral_invPowMeasure {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) : ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), f x ∂invPowMeasure = ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), (1 / ‖x‖ ^ dm1) • f x

theorem Distribution.integral_powMeasure {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (n : ℕ) (f : EuclideanSpace ℝ (Fin dm1.succ) → F) : ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), f x ∂powMeasure n = ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), ‖x‖ ^ n • f x

theorem Distribution.integral_boundMeasure {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (n : ℕ) (C1 C2 : ℝ) (C1_nonneg : 0 ≤ C1) (C2_nonneg : 0 ≤ C2) (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : MeasureTheory.Integrable f (boundMeasure n C1 C2)) : ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), f x ∂boundMeasure n C1 C2 = ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), (C1 * 1 / ‖x‖ ^ dm1 + C2 * ‖x‖ ^ n) • f x

HasTemperateGrowth of measures

theorem Distribution.invPowMeasure_integrable_pow_neg_two {dm1 : ℕ} : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => (1 + ‖x‖) ^ (-(↑dm1 + 2))) invPowMeasure

instance Distribution.instHasTemperateGrowthEuclideanSpaceRealFinSuccInvPowMeasure (dm1 : ℕ) : invPowMeasure.HasTemperateGrowth

instance Distribution.instHasTemperateGrowthEuclideanSpaceRealFinSuccPowMeasure (dm1 n : ℕ) : (powMeasure n).HasTemperateGrowth

instance Distribution.instHasTemperateGrowthEuclideanSpaceRealFinSuccBoundMeasure (dm1 n : ℕ) (C1 C2 : ℝ) : (boundMeasure n C1 C2).HasTemperateGrowth

Bounded functions as distributions

theorem Distribution.bounded_integrable {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : ∃ (c1 : ℝ) (c2 : ℝ) (n : ℕ), 0 ≤ c1 ∧ 0 ≤ c2 ∧ ∀ (x : EuclideanSpace ℝ (Fin dm1.succ)), ‖f x‖ ≤ c1 * ‖x‖ ^ (-↑dm1) + c2 * ‖x‖ ^ n) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => η x • f x) MeasureTheory.volume

def Distribution.ofBounded {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : ∃ (c1 : ℝ) (c2 : ℝ) (n : ℕ), 0 ≤ c1 ∧ 0 ≤ c2 ∧ ∀ (x : EuclideanSpace ℝ (Fin dm1.succ)), ‖f x‖ ≤ c1 * ‖x‖ ^ (-↑dm1) + c2 * ‖x‖ ^ n) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) : (EuclideanSpace ℝ (Fin dm1.succ))→d[ℝ] F

A distribution (EuclideanSpace ℝ (Fin 3)) →d[ℝ] F from a function f : EuclideanSpace ℝ (Fin 3) → F bounded by c1 * ‖x‖ ^ (-2 : ℝ) + c2 * ‖x‖ ^ n.

Equations

• Distribution.ofBounded f hf hae = SchwartzMap.mkCLMtoNormedSpace (fun (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) => ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), η x • f x) ⋯ ⋯ ⋯

theorem Distribution.ofBounded_apply {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : ∃ (c1 : ℝ) (c2 : ℝ) (n : ℕ), 0 ≤ c1 ∧ 0 ≤ c2 ∧ ∀ (x : EuclideanSpace ℝ (Fin dm1.succ)), ‖f x‖ ≤ c1 * ‖x‖ ^ (-↑dm1) + c2 * ‖x‖ ^ n) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) : (ofBounded f hf hae) η = ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), η x • f x