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

• ofFunction: Creates a distribution from a f satisfying IsDistBounded f.

def Distribution.ofFunction {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : IsDistBounded f) (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.ofFunction f hf hae = SchwartzMap.mkCLMtoNormedSpace (fun (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) => ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), η x • f x) ⋯ ⋯ ⋯

theorem Distribution.ofFunction_apply {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) : (ofFunction f hf hae) η = ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), η x • f x

@[simp]

theorem Distribution.ofFunction_zero_eq_zero {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} : ofFunction (fun (x : EuclideanSpace ℝ (Fin (dm1 + 1))) => 0) ⋯ ⋯ = 0

theorem Distribution.ofFunction_smul {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) (c : ℝ) : ofFunction (c • f) ⋯ ⋯ = c • ofFunction f hf hae

theorem Distribution.ofFunction_smul_fun {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) (c : ℝ) : ofFunction (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => c • f x) ⋯ ⋯ = c • ofFunction f hf hae

theorem Distribution.ofFunction_inner {dm1 n : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → EuclideanSpace ℝ (Fin n)) (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) (y : EuclideanSpace ℝ (Fin n)) : inner ℝ ((ofFunction f hf hae) η) y = ∫ (x : EuclideanSpace ℝ (Fin dm1.succ)), η x * inner ℝ (f x) y