Functions on Space d which can be made into distributions

i. Overview

In this module, for functions f : Space d → F, we define the property IsDistBounded f. Functions satisfying this property can be used to create distributions Space d →d[ℝ] F by integrating them against Schwartz maps.

The condition IsDistBounded f essentially says that f is bounded by a finite sum of terms of the form c * ‖x + g‖ ^ p for constants c, g and - (d - 1) ≤ p where d is the dimension of the space.

ii. Key results

• IsDistBounded : The boundedness condition on functions Space d → F for them to form distributions.
• IsDistBounded.integrable_space : If f satisfies IsDistBounded f, then fun x => η x • f x is integrable for any Schwartz map η : 𝓢(Space d, ℝ).
• IsDistBounded.integrable_time_space : If f satisfies IsDistBounded f, then fun x => η x • f x.2 is integrable for any Schwartz map η : 𝓢(Time × Space d, ℝ).
• IsDistBounded.mono : If f₁ satisfies IsDistBounded f₁ and ‖f₂ x‖ ≤ ‖f₁ x‖ for all x, then f₂ satisfies IsDistBounded f₂.

iii. Table of contents

• A. The predicate IsDistBounded f
• B. Integrability properties of functions satisfying IsDistBounded f
  • B.1. AEStronglyMeasurable conditions
  • B.2. Integrability with respect to Schwartz maps on space
  • B.3. Integrability with respect to Schwartz maps on time and space
  • B.4. Integrability with respect to inverse powers
• C. Integral on Schwartz maps is bounded by seminorms
• D. Construction rules for IsDistBounded f
  • D.1. Addition
  • D.2. Finite sums
  • D.3. Scalar multiplication
  • D.4. Components of functions
  • D.5. Compositions with additions and subtractions
  • D.6. Congruence with respect to the norm
  • D.7. Monotonicity with respect to the norm
  • D.8. Inner products
  • D.9. Scalar multiplication with constant
• E. Specific functions that are IsDistBounded
  • E.1. Constant functions
  • E.2. Powers of norms
• F. Multiplication by norms and components

iv. References

A. The predicate IsDistBounded f

def Space.IsDistBounded {F : Type} [NormedAddCommGroup F] {d : ℕ} (f : Space d → 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.

B. Integrability properties of functions satisfying IsDistBounded f

B.1. AEStronglyMeasurable conditions

theorem Space.IsDistBounded.aestronglyMeasurable {F : Type} [NormedAddCommGroup F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) : MeasureTheory.AEStronglyMeasurable (fun (x : Space d) => f x) MeasureTheory.volume

theorem Space.IsDistBounded.aeStronglyMeasurable_schwartzMap_smul {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) : MeasureTheory.AEStronglyMeasurable (fun (x : Space d) => η x • f x) MeasureTheory.volume

theorem Space.IsDistBounded.aeStronglyMeasurable_fderiv_schwartzMap_smul {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) (y : Space d) : MeasureTheory.AEStronglyMeasurable (fun (x : Space d) => (fderiv ℝ (⇑η) x) y • f x) MeasureTheory.volume

theorem Space.IsDistBounded.aeStronglyMeasurable_inv_pow {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d r : ℕ} {f : Space d → F} (hf : IsDistBounded f) : MeasureTheory.AEStronglyMeasurable (fun (x : Space d) => ‖((1 + ‖x‖) ^ r)⁻¹‖ • f x) MeasureTheory.volume

theorem Space.IsDistBounded.aeStronglyMeasurable_time_schwartzMap_smul {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : SchwartzMap (Time × Space d) ℝ) : MeasureTheory.AEStronglyMeasurable (fun (x : Time × Space d) => η x • f x.2) MeasureTheory.volume

B.2. Integrability with respect to Schwartz maps on space

theorem Space.IsDistBounded.integrable_space {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) : MeasureTheory.Integrable (fun (x : Space d) => η x • f x) MeasureTheory.volume

theorem Space.IsDistBounded.integrable_space_mul {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) : MeasureTheory.Integrable (fun (x : Space d) => η x * f x) MeasureTheory.volume

theorem Space.IsDistBounded.integrable_space_fderiv {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) (y : Space d) : MeasureTheory.Integrable (fun (x : Space d) => (fderiv ℝ (⇑η) x) y • f x) MeasureTheory.volume

theorem Space.IsDistBounded.integrable_space_fderiv_mul {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) (y : Space d) : MeasureTheory.Integrable (fun (x : Space d) => (fderiv ℝ (⇑η) x) y * f x) MeasureTheory.volume

B.3. Integrability with respect to Schwartz maps on time and space

instance Space.IsDistBounded.instHasTemperateGrowthProdProdOfOpensMeasurableSpace {D1 : Type} [NormedAddCommGroup D1] [MeasurableSpace D1] {D2 : Type} [NormedAddCommGroup D2] [MeasurableSpace D2] (μ1 : MeasureTheory.Measure D1) (μ2 : MeasureTheory.Measure D2) [μ1.HasTemperateGrowth] [μ2.HasTemperateGrowth] [OpensMeasurableSpace (D1 × D2)] : (μ1.prod μ2).HasTemperateGrowth

theorem Space.IsDistBounded.integrable_time_space {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : SchwartzMap (Time × Space d) ℝ) : MeasureTheory.Integrable (fun (x : Time × Space d) => η x • f x.2) MeasureTheory.volume

B.4. Integrability with respect to inverse powers

theorem Space.IsDistBounded.integrable_mul_inv_pow {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) : ∃ (r : ℕ), MeasureTheory.Integrable (fun (x : Space d) => ‖((1 + ‖x‖) ^ r)⁻¹‖ • f x) MeasureTheory.volume

C. Integral on Schwartz maps is bounded by seminorms

theorem Space.IsDistBounded.integral_mul_schwartzMap_bounded {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) : ∃ (s : Finset (ℕ × ℕ)) (C : ℝ), 0 ≤ C ∧ ∀ (η : SchwartzMap (Space d) ℝ), ‖∫ (x : Space d), η x • f x‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ (Space d) ℝ)) η

D. Construction rules for IsDistBounded f

theorem Space.IsDistBounded.zero {F : Type} [NormedAddCommGroup F] {d : ℕ} : IsDistBounded 0

D.1. Addition

theorem Space.IsDistBounded.add {F : Type} [NormedAddCommGroup F] {d : ℕ} {f g : Space d → F} (hf : IsDistBounded f) (hg : IsDistBounded g) : IsDistBounded (f + g)

theorem Space.IsDistBounded.fun_add {F : Type} [NormedAddCommGroup F] {d : ℕ} {f g : Space d → F} (hf : IsDistBounded f) (hg : IsDistBounded g) : IsDistBounded fun (x : Space d) => f x + g x

D.2. Finite sums

theorem Space.IsDistBounded.sum {F : Type} [NormedAddCommGroup F] {ι : Type u_1} {s : Finset ι} {d : ℕ} {f : ι → Space d → F} (hf : ∀ i ∈ s, IsDistBounded (f i)) : IsDistBounded (∑ i ∈ s, f i)

theorem Space.IsDistBounded.sum_fun {F : Type} [NormedAddCommGroup F] {ι : Type u_1} {s : Finset ι} {d : ℕ} {f : ι → Space d → F} (hf : ∀ i ∈ s, IsDistBounded (f i)) : IsDistBounded fun (x : Space d) => ∑ i ∈ s, f i x

D.3. Scalar multiplication

theorem Space.IsDistBounded.const_smul {F : Type} [NormedAddCommGroup F] {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded (c • f)

theorem Space.IsDistBounded.neg {F : Type} [NormedAddCommGroup F] {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) : IsDistBounded fun (x : Space d) => -f x

theorem Space.IsDistBounded.const_fun_smul {F : Type} [NormedAddCommGroup F] {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded fun (x : Space d) => c • f x

theorem Space.IsDistBounded.const_mul_fun {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded fun (x : Space d) => c * f x

theorem Space.IsDistBounded.mul_const_fun {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded fun (x : Space d) => f x * c

D.4. Components of functions

theorem Space.IsDistBounded.pi_comp {d n : ℕ} {f : Space d → EuclideanSpace ℝ (Fin n)} (hf : IsDistBounded f) (j : Fin n) : IsDistBounded fun (x : Space d) => (f x).ofLp j

theorem Space.IsDistBounded.vector_component {d n : ℕ} {f : Space d → Lorentz.Vector n} (hf : IsDistBounded f) (j : Fin 1 ⊕ Fin n) : IsDistBounded fun (x : Space d) => f x j

D.5. Compositions with additions and subtractions

theorem Space.IsDistBounded.comp_add_right {F : Type} [NormedAddCommGroup F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (c : Space d) : IsDistBounded fun (x : Space d) => f (x + c)

theorem Space.IsDistBounded.comp_sub_right {F : Type} [NormedAddCommGroup F] {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (c : Space d) : IsDistBounded fun (x : Space d) => f (x - c)

D.6. Congruence with respect to the norm

theorem Space.IsDistBounded.congr {F F' : Type} [NormedAddCommGroup F] [NormedAddCommGroup F'] {d : ℕ} {f : Space d → F} {g : Space d → F'} (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hfg : ∀ (x : Space d), ‖g x‖ = ‖f x‖) : IsDistBounded g

D.7. Monotonicity with respect to the norm

theorem Space.IsDistBounded.mono {F F' : Type} [NormedAddCommGroup F] [NormedAddCommGroup F'] {d : ℕ} {f : Space d → F} {g : Space d → F'} (hf : IsDistBounded f) (hae : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hfg : ∀ (x : Space d), ‖g x‖ ≤ ‖f x‖) : IsDistBounded g

D.8. Inner products

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

D.9. Scalar multiplication with constant

theorem Space.IsDistBounded.smul_const {F : Type} [NormedAddCommGroup F] {d : ℕ} [NormedSpace ℝ F] {c : Space d → ℝ} (hc : IsDistBounded c) (f : F) : IsDistBounded fun (x : Space d) => c x • f

E. Specific functions that are IsDistBounded

E.1. Constant functions

theorem Space.IsDistBounded.const {F : Type} [NormedAddCommGroup F] {d : ℕ} (f : F) : IsDistBounded fun (x : Space d) => f

E.2. Powers of norms

theorem Space.IsDistBounded.pow {d : ℕ} (n : ℤ) (hn : -↑(d - 1) ≤ n) : IsDistBounded fun (x : Space d) => ‖x‖ ^ n

theorem Space.IsDistBounded.pow_shift {d : ℕ} (n : ℤ) (g : Space d) (hn : -↑(d - 1) ≤ n) : IsDistBounded fun (x : Space d) => ‖x - g‖ ^ n

theorem Space.IsDistBounded.inv_shift {d : ℕ} (g : Space d.succ.succ) : IsDistBounded fun (x : Space d.succ.succ) => ‖x - g‖⁻¹

theorem Space.IsDistBounded.nat_pow {d : ℕ} (n : ℕ) : IsDistBounded fun (x : Space d) => ‖x‖ ^ n

theorem Space.IsDistBounded.norm_add_nat_pow {d : ℕ} (n : ℕ) (a : ℝ) : IsDistBounded fun (x : Space d) => (‖x‖ + a) ^ n

theorem Space.IsDistBounded.norm_add_pos_nat_zpow {d : ℕ} (n : ℤ) (a : ℝ) (ha : 0 < a) : IsDistBounded fun (x : Space d) => (‖x‖ + a) ^ n

theorem Space.IsDistBounded.nat_pow_shift {d : ℕ} (n : ℕ) (g : Space d) : IsDistBounded fun (x : Space d) => ‖x - g‖ ^ n

theorem Space.IsDistBounded.norm_sub {d : ℕ} (g : Space d) : IsDistBounded fun (x : Space d) => ‖x - g‖

theorem Space.IsDistBounded.norm_add {d : ℕ} (g : Space d) : IsDistBounded fun (x : Space d) => ‖x + g‖

theorem Space.IsDistBounded.inv {n : ℕ} : IsDistBounded fun (x : Space n.succ.succ) => ‖x‖⁻¹

theorem Space.IsDistBounded.norm {d : ℕ} : IsDistBounded fun (x : Space d) => ‖x‖

theorem Space.IsDistBounded.log_norm {d : ℕ} : IsDistBounded fun (x : Space d.succ.succ) => Real.log ‖x‖

theorem Space.IsDistBounded.zpow_smul_self {d : ℕ} (n : ℤ) (hn : -↑(d - 1) - 1 ≤ n) : IsDistBounded fun (x : Space d) => ‖x‖ ^ n • x

theorem Space.IsDistBounded.zpow_smul_repr_self {d : ℕ} (n : ℤ) (hn : -↑(d - 1) - 1 ≤ n) : IsDistBounded fun (x : Space d) => ‖x‖ ^ n • basis.repr x

theorem Space.IsDistBounded.zpow_smul_repr_self_sub {d : ℕ} (n : ℤ) (hn : -↑(d - 1) - 1 ≤ n) (y : Space d) : IsDistBounded fun (x : Space d) => ‖x - y‖ ^ n • basis.repr (x - y)

theorem Space.IsDistBounded.inv_pow_smul_self {d : ℕ} (n : ℕ) (hn : -↑(d - 1) - 1 ≤ -↑n) : IsDistBounded fun (x : Space d) => ‖x‖⁻¹ ^ n • x

theorem Space.IsDistBounded.inv_pow_smul_repr_self {d : ℕ} (n : ℕ) (hn : -↑(d - 1) - 1 ≤ -↑n) : IsDistBounded fun (x : Space d) => ‖x‖⁻¹ ^ n • basis.repr x

F. Multiplication by norms and components

theorem Space.IsDistBounded.norm_smul_nat_pow {d : ℕ} (p : ℕ) (c : Space d) : IsDistBounded fun (x : Space d) => ‖x‖ * ‖x + c‖ ^ p

theorem Space.IsDistBounded.norm_smul_zpow {d : ℕ} (p : ℤ) (c : Space d) (hn : -↑(d - 1) ≤ p) : IsDistBounded fun (x : Space d) => ‖x‖ * ‖x + c‖ ^ p

theorem Space.IsDistBounded.norm_smul_isDistBounded {F : Type} [NormedAddCommGroup F] {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) : IsDistBounded fun (x : Space d) => ‖x‖ • f x

theorem Space.IsDistBounded.norm_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded fun (x : Space d) => ‖x‖ * f x

theorem Space.IsDistBounded.component_smul_isDistBounded {F : Type} [NormedAddCommGroup F] {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (i : Fin d) : IsDistBounded fun (x : Space d) => x.val i • f x

theorem Space.IsDistBounded.component_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (i : Fin d) : IsDistBounded fun (x : Space d) => x.val i * f x

theorem Space.IsDistBounded.isDistBounded_smul_self {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded fun (x : Space d) => f x • x

theorem Space.IsDistBounded.isDistBounded_smul_self_repr {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded fun (x : Space d) => f x • basis.repr x

theorem Space.IsDistBounded.isDistBounded_smul_inner {F : Type} [NormedAddCommGroup F] {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (y : Space d) : IsDistBounded fun (x : Space d) => inner ℝ y x • f x

theorem Space.IsDistBounded.isDistBounded_smul_inner_of_smul_norm {F : Type} [NormedAddCommGroup F] {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded fun (x : Space d) => ‖x‖ • f x) (hae : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (y : Space d) : IsDistBounded fun (x : Space d) => inner ℝ y x • f x

theorem Space.IsDistBounded.isDistBounded_mul_inner {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (y : Space d) : IsDistBounded fun (x : Space d) => inner ℝ y x * f x

theorem Space.IsDistBounded.isDistBounded_mul_inner' {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (y : Space d) : IsDistBounded fun (x : Space d) => inner ℝ x y * f x

theorem Space.IsDistBounded.isDistBounded_mul_inner_of_smul_norm {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded fun (x : Space d) => ‖x‖ * f x) (hae : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (y : Space d) : IsDistBounded fun (x : Space d) => inner ℝ y x * f x

theorem Space.IsDistBounded.mul_inner_pow_neg_two {d : ℕ} (y : Space d.succ.succ) : IsDistBounded fun (x : Space d.succ.succ) => inner ℝ y x * ‖x‖ ^ (-2)