Bounded functions for distributions

In this module we define the property IsDistBounded f for a function f. It says that f is bounded by a finite sum of terms of the form c * ‖x + g‖ ^ p for constants c, g and -d ≤ p where d is the dimension of the space minus 1.

We prove a number of properties of these functions, inparticular that they are integrable when multiplied by a Schwartz map. This allows us to define distributions from such functions.

IsBounded

def Distribution.IsDistBounded {F : Type} [NormedAddCommGroup F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) : Prop

The boundedness condition on a function EuclideanSpace ℝ (Fin dm1.succ) → F for it to form a distribution.

Equations

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

theorem Distribution.IsDistBounded.add {F : Type} [NormedAddCommGroup F] {dm1 : ℕ} {f g : EuclideanSpace ℝ (Fin dm1.succ) → F} (hf : IsDistBounded f) (hg : IsDistBounded g) : IsDistBounded (f + g)

theorem Distribution.IsDistBounded.const_smul {F : Type} [NormedAddCommGroup F] {dm1 : ℕ} [NormedSpace ℝ F] {f : EuclideanSpace ℝ (Fin dm1.succ) → F} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded (c • f)

theorem Distribution.IsDistBounded.pi_comp {dm1 n : ℕ} {f : EuclideanSpace ℝ (Fin dm1.succ) → EuclideanSpace ℝ (Fin n)} (hf : IsDistBounded f) (j : Fin n) : IsDistBounded fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x j

theorem Distribution.IsDistBounded.comp_add_right {F : Type} [NormedAddCommGroup F] {dm1 : ℕ} {f : EuclideanSpace ℝ (Fin dm1.succ) → F} (hf : IsDistBounded f) (c : EuclideanSpace ℝ (Fin dm1.succ)) : IsDistBounded fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f (x + c)

theorem Distribution.IsDistBounded.const_mul_fun {dm1 : ℕ} {f : EuclideanSpace ℝ (Fin dm1.succ) → ℝ} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => c * f x

theorem Distribution.IsDistBounded.congr {F F' : Type} [NormedAddCommGroup F] [NormedAddCommGroup F'] {dm1 : ℕ} {f : EuclideanSpace ℝ (Fin dm1.succ) → F} {g : EuclideanSpace ℝ (Fin dm1.succ) → F'} (hf : IsDistBounded f) (hfg : ∀ (x : EuclideanSpace ℝ (Fin dm1.succ)), ‖g x‖ = ‖f x‖) : IsDistBounded g

theorem Distribution.IsDistBounded.mono {F F' : Type} [NormedAddCommGroup F] [NormedAddCommGroup F'] {dm1 : ℕ} {f : EuclideanSpace ℝ (Fin dm1.succ) → F} {g : EuclideanSpace ℝ (Fin dm1.succ) → F'} (hf : IsDistBounded f) (hfg : ∀ (x : EuclideanSpace ℝ (Fin dm1.succ)), ‖g x‖ ≤ ‖f x‖) : IsDistBounded g

theorem Distribution.IsDistBounded.inner_left {dm1 n : ℕ} {f : EuclideanSpace ℝ (Fin dm1.succ) → EuclideanSpace ℝ (Fin n)} (hf : IsDistBounded f) (y : EuclideanSpace ℝ (Fin n)) : IsDistBounded fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => inner ℝ (f x) y

Specific cases

theorem Distribution.IsDistBounded.const {F : Type} [NormedAddCommGroup F] {dm1 : ℕ} (f : F) : IsDistBounded fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f

theorem Distribution.IsDistBounded.pow {dm1 : ℕ} (n : ℤ) (hn : -↑dm1 ≤ n) : IsDistBounded fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => ‖x‖ ^ n

theorem Distribution.IsDistBounded.pow_shift {dm1 : ℕ} (n : ℤ) (g : EuclideanSpace ℝ (Fin dm1.succ)) (hn : -↑dm1 ≤ n) : IsDistBounded fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => ‖x - g‖ ^ n

theorem Distribution.IsDistBounded.inv {n : ℕ} : IsDistBounded fun (x : EuclideanSpace ℝ (Fin n.succ.succ)) => ‖x‖⁻¹

Integrability

theorem Distribution.IsDistBounded.schwartzMap_mul_integrable_norm {F : Type} [NormedAddCommGroup F] {dm1 : ℕ} {η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ} {f : EuclideanSpace ℝ (Fin dm1.succ) → F} (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => ‖η x‖ * ‖f x‖) MeasureTheory.volume

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

theorem Distribution.IsDistBounded.schwartzMap_mul_integrable {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → ℝ) (hf : IsDistBounded f) (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

theorem Distribution.IsDistBounded.integrable_fderviv_schwartzMap_mul {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → ℝ) (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) (η : SchwartzMap (EuclideanSpace ℝ (Fin dm1.succ)) ℝ) (y : EuclideanSpace ℝ (Fin dm1.succ)) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => (fderiv ℝ (⇑η) x) y * f x) MeasureTheory.volume

Integrability of 1/(1 + ‖x‖)

theorem Distribution.intergrable_pow {dm1 : ℕ} (p : ℤ) (r : ℕ) (p_bound : -↑dm1 ≤ p) (r_bound : (p + ↑dm1).toNat + invPowMeasure.integrablePower ≤ r) (v : EuclideanSpace ℝ (Fin dm1.succ)) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => ‖x + v‖ ^ p * ‖((1 + ‖x‖) ^ r)⁻¹‖) MeasureTheory.volume

theorem Distribution.IsDistBounded.norm_inv_mul_exists_pow_integrable {F : Type} [NormedAddCommGroup F] {dm1 : ℕ} (f : EuclideanSpace ℝ (Fin dm1.succ) → F) (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => f x) MeasureTheory.volume) : ∃ (r : ℕ), MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin dm1.succ)) => ‖f x‖ * ‖((1 + ‖x‖) ^ r)⁻¹‖) MeasureTheory.volume