Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.SpaceAndTime.Space.Integrals.RadialAngularMeasure public import Physlib.SpaceAndTime.Time.Basic public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic public import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

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

@[expose] public section

A. The predicate IsDistBounded f

The boundedness condition on a function Space d → F for it to form a distribution.

@[fun_prop] def IsDistBounded {d : ℕ} (f : Space d → F) : Prop := AEStronglyMeasurable (fun x => f x) volume ∧ ∃ n, ∃ c : Fin n → ℝ, ∃ g : Fin n → Space d, ∃ p : Fin n → ℤ, (∀ i, 0 ≤ c i) ∧ (∀ i, - (d - 1 : ℕ) ≤ p i) ∧ ∀ x, ‖f x‖ ≤ ∑ i, c i * ‖x + g i‖ ^ p i

B. Integrability properties of functions satisfying IsDistBounded f

B.1. AEStronglyMeasurable conditions

omit [NormedSpace ℝ F] in @[fun_prop] lemma aestronglyMeasurable {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) : AEStronglyMeasurable (fun x => f x) volume := hf.1@[fun_prop] lemma aeStronglyMeasurable_schwartzMap_smul {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) : AEStronglyMeasurable (fun x => η x • f x) := F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ AEStronglyMeasurable (fun x => η x • f x) volume All goals completed! 🐙@[fun_prop] lemma aeStronglyMeasurable_fderiv_schwartzMap_smul {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) (y : Space d) : AEStronglyMeasurable (fun x => fderiv ℝ η x y • f x) := F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fη:𝓢(Space d, ℝ)y:Space d⊢ AEStronglyMeasurable (fun x => (fderiv ℝ (⇑η) x) y • f x) volume All goals completed! 🐙@[fun_prop] lemma aeStronglyMeasurable_inv_pow {d r : ℕ} {f : Space d → F} (hf : IsDistBounded f) : AEStronglyMeasurable (fun x => ‖((1 + ‖x‖) ^ r)⁻¹‖ • f x) := AEStronglyMeasurable.smul (AEMeasurable.aestronglyMeasurable (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕr:ℕf:Space d → Fhf:IsDistBounded f⊢ AEMeasurable (fun x => ‖((1 + ‖x‖) ^ r)⁻¹‖) volume All goals completed! 🐙)) (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕr:ℕf:Space d → Fhf:IsDistBounded f⊢ AEStronglyMeasurable f volume All goals completed! 🐙)@[fun_prop] lemma aeStronglyMeasurable_time_schwartzMap_smul {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : 𝓢(Time × Space d, ℝ)) : AEStronglyMeasurable (fun x => η x • f x.2) := AEStronglyMeasurable.smul (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fη:𝓢(Time × Space d, ℝ)⊢ AEStronglyMeasurable (⇑η) volume All goals completed! 🐙) (AEStronglyMeasurable.comp_snd (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fη:𝓢(Time × Space d, ℝ)⊢ AEStronglyMeasurable f volume All goals completed! 🐙))

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

All goals completed! 🐙@[fun_prop] lemma integrable_space_mul {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) : Integrable (fun x : Space d => η x * f x) volume := d:ℕf:Space d → ℝhf:IsDistBounded fη:𝓢(Space d, ℝ)⊢ Integrable (fun x => η x * f x) volume All goals completed! 🐙@[fun_prop] lemma integrable_space_fderiv {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) (y : Space d) : Integrable (fun x : Space d => fderiv ℝ η x y • f x) volume := hf.integrable_space (LineDeriv.lineDerivOpCLM ℝ _ y η)@[fun_prop] lemma integrable_space_fderiv_mul {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) (y : Space d) : Integrable (fun x : Space d => fderiv ℝ η x y * f x) volume := hf.integrable_space (LineDeriv.lineDerivOpCLM ℝ _ y η)

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

All goals completed! 🐙 𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ ((1 + ‖x‖) ^ rt1)⁻¹ * ((1 + ‖x‖) ^ rt2)⁻¹ ≤ ((1 + ‖x.1‖) ^ rt1)⁻¹ * ((1 + ‖x.2‖) ^ rt2)⁻¹ apply mul_le_mul _ _ (𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ 0 ≤ ((1 + ‖x‖) ^ rt2)⁻¹ All goals completed! 🐙) (𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ 0 ≤ ((1 + ‖x.1‖) ^ rt1)⁻¹ All goals completed! 🐙) 𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ ((1 + ‖x‖) ^ rt1)⁻¹ ≤ ((1 + ‖x.1‖) ^ rt1)⁻¹ exact inv_anti₀ (𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ 0 < (1 + ‖x.1‖) ^ rt1 All goals completed! 🐙) (pow_le_pow_left₀ (𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ 0 ≤ 1 + ‖x.1‖ All goals completed! 🐙) (𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ 1 + ‖x.1‖ ≤ 1 + ‖x‖ All goals completed! 🐙) rt1) 𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ ((1 + ‖x‖) ^ rt2)⁻¹ ≤ ((1 + ‖x.2‖) ^ rt2)⁻¹ exact inv_anti₀ (𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ 0 < (1 + ‖x.2‖) ^ rt2 All goals completed! 🐙) (pow_le_pow_left₀ (𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ 0 ≤ 1 + ‖x.2‖ All goals completed! 🐙) (𝕜:TypeE:TypeF:TypeF':Typeinst✝¹³:RCLike 𝕜inst✝¹²:NormedAddCommGroup Einst✝¹¹:NormedAddCommGroup Finst✝¹⁰:NormedAddCommGroup F'inst✝⁹:NormedSpace ℝ Finst✝⁸:NormedSpace ℝ F'inst✝⁷:NormedSpace ℝ ED1:Typeinst✝⁶:NormedAddCommGroup D1inst✝⁵:MeasurableSpace D1D2:Typeinst✝⁴:NormedAddCommGroup D2inst✝³:MeasurableSpace D2μ1:Measure D1μ2:Measure D2inst✝²:μ1.HasTemperateGrowthinst✝¹:μ2.HasTemperateGrowthinst✝:OpensMeasurableSpace (D1 × D2)rt1:ℕh1:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt1)) μ1rt2:ℕh2:Integrable (fun x => (1 + ‖x‖) ^ (-↑rt2)) μ2x:D1 × D2⊢ 1 + ‖x.2‖ ≤ 1 + ‖x‖ All goals completed! 🐙) rt2)F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fη✝:𝓢(Time × Space d, ℝ)p:ℤhp✝:-↑(d - 1) ≤ pη:𝓢(Time × Space d, ℝ)hp:¬p = 0x:Time × Space d⊢ ‖x.2‖ ^ (p + ↑(d - 1)) * |η x| ≤ ‖x‖ ^ (p + ↑(d - 1)) * |η x| exact mul_le_mul_of_nonneg_right (zpow_le_zpow_left₀ (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fη✝:𝓢(Time × Space d, ℝ)p:ℤhp✝:-↑(d - 1) ≤ pη:𝓢(Time × Space d, ℝ)hp:¬p = 0x:Time × Space d⊢ 0 ≤ p + ↑(d - 1) All goals completed! 🐙) (norm_nonneg _) (norm_snd_le x)) (abs_nonneg _)

B.4. Integrability with respect to inverse powers

F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd✝:ℕd:ℕf:Space (d + 1) → Fhf:IsDistBounded fm:ℕ := radialAngularMeasure.integrablePowerq:ℕv:Space (d + 1)hr1:∀ (x : Space (d + 1)), ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹x:Space (d + 1)⊢ ‖x‖ ^ (q + radialAngularMeasure.integrablePower) * ((1 + ‖x - v‖) ^ (q + m))⁻¹ ≤ (1 + ‖v‖) ^ (q + m) refine mul_inv_le_of_le_mul₀ ?_ (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd✝:ℕd:ℕf:Space (d + 1) → Fhf:IsDistBounded fm:ℕ := radialAngularMeasure.integrablePowerq:ℕv:Space (d + 1)hr1:∀ (x : Space (d + 1)), ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹x:Space (d + 1)⊢ 0 ≤ (1 + ‖v‖) ^ (q + m) All goals completed! 🐙) ?_ F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd✝:ℕd:ℕf:Space (d + 1) → Fhf:IsDistBounded fm:ℕ := radialAngularMeasure.integrablePowerq:ℕv:Space (d + 1)hr1:∀ (x : Space (d + 1)), ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹x:Space (d + 1)⊢ 0 ≤ (1 + ‖x - v‖) ^ (q + m) All goals completed! 🐙 F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd✝:ℕd:ℕf:Space (d + 1) → Fhf:IsDistBounded fm:ℕ := radialAngularMeasure.integrablePowerq:ℕv:Space (d + 1)hr1:∀ (x : Space (d + 1)), ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹x:Space (d + 1)⊢ ‖x‖ ^ (q + m) ≤ (1 + ‖v‖) ^ (q + m) * (1 + ‖x - v‖) ^ (q + m) calc ‖x‖ ^ (q + m) ≤ ((1 + ‖v‖) * (1 + ‖x - v‖)) ^ (q + m) := F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd✝:ℕd:ℕf:Space (d + 1) → Fhf:IsDistBounded fm:ℕ := radialAngularMeasure.integrablePowerq:ℕv:Space (d + 1)hr1:∀ (x : Space (d + 1)), ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹x:Space (d + 1)⊢ ‖x‖ ^ (q + m) ≤ ((1 + ‖v‖) * (1 + ‖x - v‖)) ^ (q + m) F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd✝:ℕd:ℕf:Space (d + 1) → Fhf:IsDistBounded fm:ℕ := radialAngularMeasure.integrablePowerq:ℕv:Space (d + 1)hr1:∀ (x : Space (d + 1)), ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹x:Space (d + 1)⊢ ‖x‖ ≤ (1 + ‖v‖) * (1 + ‖x - v‖) All goals completed! 🐙 _ = (1 + ‖v‖) ^ (q + m) * (1 + ‖x - v‖) ^ (q + m) := mul_pow _ _ _ F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd✝:ℕd:ℕf:Space (d + 1) → Fhf:IsDistBounded fm:ℕ := radialAngularMeasure.integrablePowerq:ℕv:Space (d + 1)hr1:∀ (x : Space (d + 1)), ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹⊢ AEStronglyMeasurable (fun x => ((1 + ‖x - v‖) ^ (q + m))⁻¹) radialAngularMeasure exact Measurable.aestronglyMeasurable (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd✝:ℕd:ℕf:Space (d + 1) → Fhf:IsDistBounded fm:ℕ := radialAngularMeasure.integrablePowerq:ℕv:Space (d + 1)hr1:∀ (x : Space (d + 1)), ‖((1 + ‖x - v‖) ^ (q + m))⁻¹‖ = ((1 + ‖x - v‖) ^ (q + m))⁻¹⊢ Measurable fun x => ((1 + ‖x - v‖) ^ (q + m))⁻¹ All goals completed! 🐙)

C. Integral on Schwartz maps is bounded by seminorms

All goals completed! 🐙

D. Construction rules for IsDistBounded f

@[fun_prop] lemma zero {d} : IsDistBounded (0 : Space d → F) := ⟨F:Typeinst✝:NormedAddCommGroup Fd:ℕ⊢ AEStronglyMeasurable (fun x => 0 x) volume All goals completed! 🐙, 1, fun _ => 0, fun _ => 0, fun _ => 0, F:Typeinst✝:NormedAddCommGroup Fd:ℕ⊢ (∀ (i : Fin 1), 0 ≤ (fun x => 0) i) ∧ (∀ (i : Fin 1), -↑(d - 1) ≤ (fun x => 0) i) ∧ ∀ (x : Space d), ‖0 x‖ ≤ ∑ i, (fun x => 0) i * ‖x + (fun x => 0) i‖ ^ (fun x => 0) i All goals completed! 🐙⟩

D.1. Addition

@[fun_prop] lemma add {d : ℕ} {f g : Space d → F} (hf : IsDistBounded f) (hg : IsDistBounded g) : IsDistBounded (f + g) := F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhf:IsDistBounded fhg:IsDistBounded g⊢ IsDistBounded (f + g) F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhg:IsDistBounded ghae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ IsDistBounded (f + g) F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 i⊢ IsDistBounded (f + g) refine ⟨F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 i⊢ AEStronglyMeasurable (fun x => (f + g) x) volume All goals completed! 🐙, n1 + n2, Fin.append c1 c2, Fin.append g1 g2, Fin.append p1 p2, ?_, ?_, ?_⟩ F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 i⊢ ∀ (i : Fin (n1 + n2)), 0 ≤ Fin.append c1 c2 i F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 ii:Fin (n1 + n2)⊢ 0 ≤ Fin.append c1 c2 i induction i using Fin.addCases with F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 ii:Fin n1⊢ 0 ≤ Fin.append c1 c2 (Fin.castAdd n2 i) All goals completed! 🐙 F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 ii:Fin n2⊢ 0 ≤ Fin.append c1 c2 (Fin.natAdd n1 i) All goals completed! 🐙 F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 i⊢ ∀ (i : Fin (n1 + n2)), -↑(d - 1) ≤ Fin.append p1 p2 i F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 ii:Fin (n1 + n2)⊢ -↑(d - 1) ≤ Fin.append p1 p2 i induction i using Fin.addCases with F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 ii:Fin n1⊢ -↑(d - 1) ≤ Fin.append p1 p2 (Fin.castAdd n2 i) All goals completed! 🐙 F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 ii:Fin n2⊢ -↑(d - 1) ≤ Fin.append p1 p2 (Fin.natAdd n1 i) All goals completed! 🐙 F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 i⊢ ∀ (x : Space d), ‖(f + g) x‖ ≤ ∑ i, Fin.append c1 c2 i * ‖x + Fin.append g1 g2 i‖ ^ Fin.append p1 p2 i F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 ix:Space d⊢ ‖(f + g) x‖ ≤ ∑ i, Fin.append c1 c2 i * ‖x + Fin.append g1 g2 i‖ ^ Fin.append p1 p2 i F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ihae2:AEStronglyMeasurable (fun x => g x) volumen2:ℕc2:Fin n2 → ℝg2:Fin n2 → Space dp2:Fin n2 → ℤc2_nonneg:∀ (i : Fin n2), 0 ≤ c2 ip2_bound:∀ (i : Fin n2), -↑(d - 1) ≤ p2 ibound2:∀ (x : Space d), ‖g x‖ ≤ ∑ i, c2 i * ‖x + g2 i‖ ^ p2 ix:Space d⊢ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i + ∑ i, c2 i * ‖x + g2 i‖ ^ p2 i = ∑ i, Fin.append c1 c2 i * ‖x + Fin.append g1 g2 i‖ ^ Fin.append p1 p2 i All goals completed! 🐙@[fun_prop] lemma fun_add {d : ℕ} {f g : Space d → F} (hf : IsDistBounded f) (hg : IsDistBounded g) : IsDistBounded (fun x => f x + g x) := F:Typeinst✝:NormedAddCommGroup Fd:ℕf:Space d → Fg:Space d → Fhf:IsDistBounded fhg:IsDistBounded g⊢ IsDistBounded fun x => f x + g x All goals completed! 🐙

D.2. Finite sums

F:Typeinst✝:NormedAddCommGroup Fι:Type u_1d:ℕf:ι → Space d → Fi:ιs:Finset ιhi:i ∉ sih:(∀ i ∈ s, IsDistBounded (f i)) → IsDistBounded (∑ i ∈ s, f i)hf:∀ i_1 ∈ insert i s, IsDistBounded (f i_1)⊢ IsDistBounded (f i + ∑ x ∈ s, f x) All goals completed! 🐙lemma sum_fun {ι : Type*} {s : Finset ι} {d : ℕ} {f : ι → Space d → F} (hf : ∀ i ∈ s, IsDistBounded (f i)) : IsDistBounded (fun x => ∑ i ∈ s, f i x) := Finset.sum_fn s f ▸ sum hf

D.3. Scalar multiplication

@[fun_prop] lemma const_smul {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded (c • f) := F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fc:ℝ⊢ IsDistBounded (c • f) F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fc:ℝhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ IsDistBounded (c • f) refine ⟨F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fc:ℝhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ AEStronglyMeasurable (fun x => (c • f) x) volume All goals completed! 🐙, n1, ‖c‖ • c1, g1, p1, fun i => mul_nonneg (norm_nonneg c) (c1_nonneg i), p1_bound, fun x => ?_⟩ F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fc:ℝhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ix:Space d⊢ ‖c‖ * ‖f x‖ ≤ ‖c‖ * ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i All goals completed! 🐙@[fun_prop] lemma neg {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) : IsDistBounded (fun x => - f x) := F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded f⊢ IsDistBounded fun x => -f x All goals completed! 🐙@[fun_prop] lemma const_fun_smul {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded (fun x => c • f x) := hf.const_smul c@[fun_prop] lemma const_mul_fun {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded (fun x => c * f x) := hf.const_smul c@[fun_prop] lemma mul_const_fun {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (c : ℝ) : IsDistBounded (fun x => f x * c) := d:ℕf:Space d → ℝhf:IsDistBounded fc:ℝ⊢ IsDistBounded fun x => f x * c All goals completed! 🐙

D.4. Components of functions

@[fun_prop] lemma pi_comp {d n : ℕ} {f : Space d → EuclideanSpace ℝ (Fin n)} (hf : IsDistBounded f) (j : Fin n) : IsDistBounded (fun x => f x j) := d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)hf:IsDistBounded fj:Fin n⊢ IsDistBounded fun x => (f x).ofLp j d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)j:Fin nhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ IsDistBounded fun x => (f x).ofLp j exact ⟨d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)j:Fin nhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ AEStronglyMeasurable (fun x => (fun x => (f x).ofLp j) x) volume All goals completed! 🐙, n1, c1, g1, p1, c1_nonneg, p1_bound, fun x => (PiLp.norm_apply_le (f x) j).trans (bound1 x)⟩lemma vector_component {d n : ℕ} {f : Space d → Lorentz.Vector n} (hf : IsDistBounded f) (j : Fin 1 ⊕ Fin n) : IsDistBounded (fun x => f x j) := d:ℕn:ℕf:Space d → Lorentz.Vector nhf:IsDistBounded fj:Fin 1 ⊕ Fin n⊢ IsDistBounded fun x => f x j d:ℕn:ℕf:Space d → Lorentz.Vector nj:Fin 1 ⊕ Fin nhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ IsDistBounded fun x => f x j refine ⟨d:ℕn:ℕf:Space d → Lorentz.Vector nj:Fin 1 ⊕ Fin nhae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ AEStronglyMeasurable (fun x => (fun x => f x j) x) volume All goals completed! 🐙, n1, c1, g1, p1, c1_nonneg, p1_bound, fun x => le_trans ?_ (bound1 x)⟩ All goals completed! 🐙

D.5. Compositions with additions and subtractions

All goals completed! 🐙lemma comp_sub_right {d : ℕ} {f : Space d → F} (hf : IsDistBounded f) (c : Space d) : IsDistBounded (fun x => f (x - c)) := hf.comp_add_right (- c)

D.6. Congruence with respect to the norm

omit [NormedSpace ℝ F'] in lemma congr {d : ℕ} {f : Space d → F} {g : Space d → F'} (hf : IsDistBounded f) (hae : AEStronglyMeasurable g) (hfg : ∀ x, ‖g x‖ = ‖f x‖) : IsDistBounded g := F:TypeF':Typeinst✝¹:NormedAddCommGroup Finst✝:NormedAddCommGroup F'd:ℕf:Space d → Fg:Space d → F'hf:IsDistBounded fhae:AEStronglyMeasurable g volumehfg:∀ (x : Space d), ‖g x‖ = ‖f x‖⊢ IsDistBounded g F:TypeF':Typeinst✝¹:NormedAddCommGroup Finst✝:NormedAddCommGroup F'd:ℕf:Space d → Fg:Space d → F'hae:AEStronglyMeasurable g volumehfg:∀ (x : Space d), ‖g x‖ = ‖f x‖hae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ IsDistBounded g All goals completed! 🐙

D.7. Monotonicity with respect to the norm

omit [NormedSpace ℝ F'] in lemma mono {d : ℕ} {f : Space d → F} {g : Space d → F'} (hf : IsDistBounded f) (hae : AEStronglyMeasurable g) (hfg : ∀ x, ‖g x‖ ≤ ‖f x‖) : IsDistBounded g := F:TypeF':Typeinst✝¹:NormedAddCommGroup Finst✝:NormedAddCommGroup F'd:ℕf:Space d → Fg:Space d → F'hf:IsDistBounded fhae:AEStronglyMeasurable g volumehfg:∀ (x : Space d), ‖g x‖ ≤ ‖f x‖⊢ IsDistBounded g F:TypeF':Typeinst✝¹:NormedAddCommGroup Finst✝:NormedAddCommGroup F'd:ℕf:Space d → Fg:Space d → F'hae:AEStronglyMeasurable g volumehfg:∀ (x : Space d), ‖g x‖ ≤ ‖f x‖hae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ IsDistBounded g All goals completed! 🐙

D.8. Inner products

@[fun_prop] lemma inner_left {d n : ℕ} {f : Space d → EuclideanSpace ℝ (Fin n) } (hf : IsDistBounded f) (y : EuclideanSpace ℝ (Fin n)) : IsDistBounded (fun x => ⟪f x, y⟫_ℝ) := d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)hf:IsDistBounded fy:EuclideanSpace ℝ (Fin n)⊢ IsDistBounded fun x => ⟪f x, y⟫_ℝ d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)y:EuclideanSpace ℝ (Fin n)hae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ IsDistBounded fun x => ⟪f x, y⟫_ℝ refine ⟨d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)y:EuclideanSpace ℝ (Fin n)hae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i⊢ AEStronglyMeasurable (fun x => (fun x => ⟪f x, y⟫_ℝ) x) volume All goals completed! 🐙, n1, fun i => ‖y‖ * c1 i, g1, p1, fun i => mul_nonneg (norm_nonneg y) (c1_nonneg i), p1_bound, fun x => ?_⟩ d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)y:EuclideanSpace ℝ (Fin n)hae1:AEStronglyMeasurable (fun x => f x) volumen1:ℕc1:Fin n1 → ℝg1:Fin n1 → Space dp1:Fin n1 → ℤc1_nonneg:∀ (i : Fin n1), 0 ≤ c1 ip1_bound:∀ (i : Fin n1), -↑(d - 1) ≤ p1 ibound1:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c1 i * ‖x + g1 i‖ ^ p1 ix:Space d⊢ ‖⟪f x, y⟫_ℝ‖ ≤ ‖y‖ * ∑ i, c1 i * ‖x + g1 i‖ ^ p1 i All goals completed! 🐙

D.9. Scalar multiplication with constant

@[fun_prop] lemma smul_const {d : ℕ} [NormedSpace ℝ F] {c : Space d → ℝ} (hc : IsDistBounded c) (f : F) : IsDistBounded (fun x => c x • f) := (hc.mul_const_fun ‖f‖).congr (F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Fc:Space d → ℝhc:IsDistBounded cf:F⊢ AEStronglyMeasurable (fun x => c x • f) volume All goals completed! 🐙) fun x => F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Fc:Space d → ℝhc:IsDistBounded cf:Fx:Space d⊢ ‖c x • f‖ = ‖c x * ‖f‖‖ All goals completed! 🐙

E. Specific functions that are IsDistBounded

E.1. Constant functions

@[fun_prop] lemma const {d : ℕ} (f : F) : IsDistBounded (d := d) (fun _ : Space d => f) := ⟨F:Typeinst✝:NormedAddCommGroup Fd:ℕf:F⊢ AEStronglyMeasurable (fun x => (fun x => f) x) volume All goals completed! 🐙, 1, fun _ => ‖f‖, fun _ => 0, fun _ => 0, F:Typeinst✝:NormedAddCommGroup Fd:ℕf:F⊢ (∀ (i : Fin 1), 0 ≤ (fun x => ‖f‖) i) ∧ (∀ (i : Fin 1), -↑(d - 1) ≤ (fun x => 0) i) ∧ ∀ (x : Space d), ‖(fun x => f) x‖ ≤ ∑ i, (fun x => ‖f‖) i * ‖x + (fun x => 0) i‖ ^ (fun x => 0) i All goals completed! 🐙⟩

E.2. Powers of norms

@[fun_prop] lemma pow {d : ℕ} (n : ℤ) (hn : - (d - 1 : ℕ) ≤ n) : IsDistBounded (d := d) (fun x => ‖x‖ ^ n) := ⟨AEMeasurable.aestronglyMeasurable (d:ℕn:ℤhn:-↑(d - 1) ≤ n⊢ AEMeasurable (fun x => (fun x => ‖x‖ ^ n) x) volume All goals completed! 🐙), 1, fun _ => 1, fun _ => 0, fun _ => n, fun _ => zero_le_one, fun _ => hn, fun x => d:ℕn:ℤhn:-↑(d - 1) ≤ nx:Space d⊢ ‖(fun x => ‖x‖ ^ n) x‖ ≤ ∑ i, (fun x => 1) i * ‖x + (fun x => 0) i‖ ^ (fun x => n) i All goals completed! 🐙⟩@[fun_prop] lemma pow_shift {d : ℕ} (n : ℤ) (g : Space d) (hn : - (d - 1 : ℕ) ≤ n) : IsDistBounded (d := d) (fun x => ‖x - g‖ ^ n) := ⟨AEMeasurable.aestronglyMeasurable (d:ℕn:ℤg:Space dhn:-↑(d - 1) ≤ n⊢ AEMeasurable (fun x => (fun x => ‖x - g‖ ^ n) x) volume All goals completed! 🐙), 1, fun _ => 1, fun _ => - g, fun _ => n, fun _ => zero_le_one, fun _ => hn, fun x => d:ℕn:ℤg:Space dhn:-↑(d - 1) ≤ nx:Space d⊢ ‖(fun x => ‖x - g‖ ^ n) x‖ ≤ ∑ i, (fun x => 1) i * ‖x + (fun x => -g) i‖ ^ (fun x => n) i All goals completed! 🐙⟩@[fun_prop] lemma inv_shift {d : ℕ} (g : Space d) (hd : 2 ≤ d := by omega) : IsDistBounded (d := d) (fun x => ‖x - g‖⁻¹) := d:ℕg:Space dhd:2 ≤ d⊢ IsDistBounded fun x => ‖x - g‖⁻¹ simpa using IsDistBounded.pow_shift (d := d) (-1) g (d:ℕg:Space dhd:2 ≤ d⊢ -↑(d - 1) ≤ -1 All goals completed! 🐙)@[fun_prop] lemma nat_pow {d : ℕ} (n : ℕ) : IsDistBounded (d := d) (fun x => ‖x‖ ^ n) := d:ℕn:ℕ⊢ IsDistBounded fun x => ‖x‖ ^ n exact IsDistBounded.pow (d := d) (n : ℤ) (d:ℕn:ℕ⊢ -↑(d - 1) ≤ ↑n All goals completed! 🐙)@[fun_prop] lemma norm_add_nat_pow {d : ℕ} (n : ℕ) (a : ℝ) : IsDistBounded (d := d) (fun x => (‖x‖ + a) ^ n) := d:ℕn:ℕa:ℝ⊢ IsDistBounded fun x => (‖x‖ + a) ^ n d:ℕn:ℕa:ℝ⊢ IsDistBounded fun x => ∑ m ∈ Finset.range (n + 1), ‖x‖ ^ m * a ^ (n - m) * ↑(n.choose m) exact sum_fun fun i _ => d:ℕn:ℕa:ℝi:ℕx✝:i ∈ Finset.range (n + 1)⊢ IsDistBounded fun x => ‖x‖ ^ i * a ^ (n - i) * ↑(n.choose i) All goals completed! 🐙@[fun_prop] lemma norm_add_pos_nat_zpow {d : ℕ} (n : ℤ) (a : ℝ) (ha : 0 < a) : IsDistBounded (d := d) (fun x => (‖x‖ + a) ^ n) := d:ℕn:ℤa:ℝha:0 < a⊢ IsDistBounded fun x => (‖x‖ + a) ^ n match n with d:ℕn✝:ℤa:ℝha:0 < an:ℕ⊢ IsDistBounded fun x => (‖x‖ + a) ^ Int.ofNat n All goals completed! 🐙 d:ℕn✝:ℤa:ℝha:0 < an:ℕ⊢ IsDistBounded fun x => (‖x‖ + a) ^ Int.negSucc n refine IsDistBounded.mono (f := fun x => (a ^ ((n + 1)))⁻¹) (d:ℕn✝:ℤa:ℝha:0 < an:ℕ⊢ IsDistBounded fun x => (a ^ (n + 1))⁻¹ All goals completed! 🐙) (AEMeasurable.aestronglyMeasurable (d:ℕn✝:ℤa:ℝha:0 < an:ℕ⊢ AEMeasurable (fun x => (‖x‖ + a) ^ Int.negSucc n) volume All goals completed! 🐙)) fun x => ?_ d:ℕn✝:ℤa:ℝha:0 < an:ℕx:Space d⊢ ((‖x‖ + a) ^ (n + 1))⁻¹ ≤ (a ^ (n + 1))⁻¹ exact inv_anti₀ (d:ℕn✝:ℤa:ℝha:0 < an:ℕx:Space d⊢ 0 < a ^ (n + 1) All goals completed! 🐙) (pow_le_pow_left₀ ha.le (d:ℕn✝:ℤa:ℝha:0 < an:ℕx:Space d⊢ a ≤ ‖x‖ + a All goals completed! 🐙) _)@[fun_prop] lemma nat_pow_shift {d : ℕ} (n : ℕ) (g : Space d) : IsDistBounded (d := d) (fun x => ‖x - g‖ ^ n) := IsDistBounded.pow_shift (d := d) (n : ℤ) g (d:ℕn:ℕg:Space d⊢ -↑(d - 1) ≤ ↑n All goals completed! 🐙)@[fun_prop] lemma norm_sub {d : ℕ} (g : Space d) : IsDistBounded (d := d) (fun x => ‖x - g‖) := d:ℕg:Space d⊢ IsDistBounded fun x => ‖x - g‖ All goals completed! 🐙@[fun_prop] lemma norm_add {d : ℕ} (g : Space d) : IsDistBounded (d := d) (fun x => ‖x + g‖) := d:ℕg:Space d⊢ IsDistBounded fun x => ‖x + g‖ All goals completed! 🐙@[fun_prop] lemma inv {d : ℕ} (hd: 2 ≤ d := by omega): IsDistBounded (d := d) (fun x => ‖x‖⁻¹) := d:ℕhd:2 ≤ d⊢ IsDistBounded fun x => ‖x‖⁻¹ simpa using IsDistBounded.pow (d := d) (-1) (d:ℕhd:2 ≤ d⊢ -↑(d - 1) ≤ -1 All goals completed! 🐙)@[fun_prop] lemma norm {d : ℕ} : IsDistBounded (d := d) (fun x => ‖x‖) := d:ℕ⊢ IsDistBounded fun x => ‖x‖ All goals completed! 🐙d:ℕhd:2 ≤ dx:Space dh1:-‖x‖⁻¹ ≤ Real.log ‖x‖h2:Real.log ‖x‖ ≤ ‖x‖⊢ Real.log ‖x‖ ≤ ‖x‖⁻¹ + ‖x‖ ∧ -Real.log ‖x‖ ≤ ‖x‖⁻¹ + ‖x‖ d:ℕhd:2 ≤ dx:Space dh1:-‖x‖⁻¹ ≤ Real.log ‖x‖h2:Real.log ‖x‖ ≤ ‖x‖⊢ Real.log ‖x‖ ≤ ‖x‖⁻¹ + ‖x‖d:ℕhd:2 ≤ dx:Space dh1:-‖x‖⁻¹ ≤ Real.log ‖x‖h2:Real.log ‖x‖ ≤ ‖x‖⊢ -Real.log ‖x‖ ≤ ‖x‖⁻¹ + ‖x‖ d:ℕhd:2 ≤ dx:Space dh1:-‖x‖⁻¹ ≤ Real.log ‖x‖h2:Real.log ‖x‖ ≤ ‖x‖⊢ Real.log ‖x‖ ≤ ‖x‖⁻¹ + ‖x‖ exact h2.trans (d:ℕhd:2 ≤ dx:Space dh1:-‖x‖⁻¹ ≤ Real.log ‖x‖h2:Real.log ‖x‖ ≤ ‖x‖⊢ ‖x‖ ≤ ‖x‖⁻¹ + ‖x‖ All goals completed! 🐙) d:ℕhd:2 ≤ dx:Space dh1:-‖x‖⁻¹ ≤ Real.log ‖x‖h2:Real.log ‖x‖ ≤ ‖x‖⊢ -Real.log ‖x‖ ≤ ‖x‖⁻¹ + ‖x‖ All goals completed! 🐙lemma zpow_smul_self {d : ℕ} (n : ℤ) (hn : - (d - 1 : ℕ) - 1 ≤ n) : IsDistBounded (d := d) (fun x => ‖x‖ ^ n • x) := d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ n⊢ IsDistBounded fun x => ‖x‖ ^ n • x d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:n = -1⊢ IsDistBounded fun x => ‖x‖ ^ n • xd:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:¬n = -1⊢ IsDistBounded fun x => ‖x‖ ^ n • x d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:n = -1⊢ IsDistBounded fun x => ‖x‖ ^ n • x d:ℕhn:-↑(d - 1) - 1 ≤ -1⊢ IsDistBounded fun x => ‖x‖ ^ (-1) • x refine IsDistBounded.mono (f := fun x => (1 : ℝ)) (d:ℕhn:-↑(d - 1) - 1 ≤ -1⊢ IsDistBounded fun x => 1 All goals completed! 🐙) (AEMeasurable.aestronglyMeasurable (d:ℕhn:-↑(d - 1) - 1 ≤ -1⊢ AEMeasurable (fun x => ‖x‖ ^ (-1) • x) volume All goals completed! 🐙)) fun x => ?_ All goals completed! 🐙 refine IsDistBounded.congr (f := fun x => ‖x‖ ^ (n + 1)) (pow _ (d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:¬n = -1⊢ -↑(d - 1) ≤ n + 1 All goals completed! 🐙)) (AEMeasurable.aestronglyMeasurable (d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:¬n = -1⊢ AEMeasurable (fun x => ‖x‖ ^ n • x) volume All goals completed! 🐙)) fun x => ?_ d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:¬n = -1⊢ ‖‖0‖ ^ n • 0‖ = ‖‖0‖ ^ (n + 1)‖d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:¬n = -1x:Space dhx:x ≠ 0⊢ ‖‖x‖ ^ n • x‖ = ‖‖x‖ ^ (n + 1)‖ d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:¬n = -1⊢ ‖‖0‖ ^ n • 0‖ = ‖‖0‖ ^ (n + 1)‖ All goals completed! 🐙 d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nhzero:¬n = -1x:Space dhx:x ≠ 0⊢ ‖‖x‖ ^ n • x‖ = ‖‖x‖ ^ (n + 1)‖ All goals completed! 🐙lemma zpow_smul_repr_self {d : ℕ} (n : ℤ) (hn : - (d - 1 : ℕ) - 1 ≤ n) : IsDistBounded (d := d) (fun x => ‖x‖ ^ n • basis.repr x) := (zpow_smul_self n hn).congr (AEMeasurable.aestronglyMeasurable (d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ n⊢ AEMeasurable (fun x => ‖x‖ ^ n • basis.repr x) volume All goals completed! 🐙)) fun x => d:ℕn:ℤhn:-↑(d - 1) - 1 ≤ nx:Space d⊢ ‖‖x‖ ^ n • basis.repr x‖ = ‖‖x‖ ^ n • x‖ All goals completed! 🐙lemma zpow_smul_repr_self_sub {d : ℕ} (n : ℤ) (hn : - (d - 1 : ℕ) - 1 ≤ n) (y : Space d) : IsDistBounded (d := d) (fun x => ‖x - y‖ ^ n • basis.repr (x - y)) := (zpow_smul_repr_self n hn).comp_sub_right ylemma inv_pow_smul_self {d : ℕ} (n : ℕ) (hn : - (d - 1 : ℕ) - 1 ≤ (- n : ℤ)) : IsDistBounded (d := d) (fun x => ‖x‖⁻¹ ^ n • x) := d:ℕn:ℕhn:-↑(d - 1) - 1 ≤ -↑n⊢ IsDistBounded fun x => ‖x‖⁻¹ ^ n • x simpa using zpow_smul_self (n := - (n : ℤ)) (d:ℕn:ℕhn:-↑(d - 1) - 1 ≤ -↑n⊢ -↑(d - 1) - 1 ≤ -↑n All goals completed! 🐙)lemma inv_pow_smul_repr_self {d : ℕ} (n : ℕ) (hn : - (d - 1 : ℕ) - 1 ≤ (- n : ℤ)) : IsDistBounded (d := d) (fun x => ‖x‖⁻¹ ^ n • basis.repr x) := d:ℕn:ℕhn:-↑(d - 1) - 1 ≤ -↑n⊢ IsDistBounded fun x => ‖x‖⁻¹ ^ n • basis.repr x simpa using zpow_smul_repr_self (n := - (n : ℤ)) (d:ℕn:ℕhn:-↑(d - 1) - 1 ≤ -↑n⊢ -↑(d - 1) - 1 ≤ -↑n All goals completed! 🐙)

F. Multiplication by norms and components

d:ℕp:ℕc:Space dx:Space d⊢ ‖x‖ * ‖x + c‖ ^ p ≤ ‖x‖ * (‖x‖ + ‖c‖) ^ p d:ℕp:ℕc:Space dx:Space d⊢ ‖x + c‖ ≤ ‖x‖ + ‖c‖ All goals completed! 🐙d:ℕp✝:ℤc:Space dp:ℕhn:-↑(d - 1) ≤ Int.negSucc php:¬p = 0x:Space d⊢ ‖x‖ * (‖x‖ ^ (p + 1))⁻¹ = (‖x‖ ^ p)⁻¹ d:ℕp✝:ℤc:Space dp:ℕhn:-↑(d - 1) ≤ Int.negSucc php:¬p = 0x:Space dhx:‖x‖ = 0⊢ ‖x‖ * (‖x‖ ^ (p + 1))⁻¹ = (‖x‖ ^ p)⁻¹d:ℕp✝:ℤc:Space dp:ℕhn:-↑(d - 1) ≤ Int.negSucc php:¬p = 0x:Space dhx:‖x‖ ≠ 0⊢ ‖x‖ * (‖x‖ ^ (p + 1))⁻¹ = (‖x‖ ^ p)⁻¹ d:ℕp✝:ℤc:Space dp:ℕhn:-↑(d - 1) ≤ Int.negSucc php:¬p = 0x:Space dhx:‖x‖ = 0⊢ ‖x‖ * (‖x‖ ^ (p + 1))⁻¹ = (‖x‖ ^ p)⁻¹ All goals completed! 🐙 d:ℕp✝:ℤc:Space dp:ℕhn:-↑(d - 1) ≤ Int.negSucc php:¬p = 0x:Space dhx:‖x‖ ≠ 0⊢ ‖x‖ * (‖x‖ ^ (p + 1))⁻¹ = (‖x‖ ^ p)⁻¹ d:ℕp✝:ℤc:Space dp:ℕhn:-↑(d - 1) ≤ Int.negSucc php:¬p = 0x:Space dhx:‖x‖ ≠ 0⊢ ‖x‖ * ‖x‖ ^ p = ‖x‖ ^ (p + 1) All goals completed! 🐙F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhae:AEStronglyMeasurable (fun x => f x) volumen:ℕc:Fin n → ℝg:Fin n → Space dp:Fin n → ℤc_nonneg:∀ (i : Fin n), 0 ≤ c ip_bound:∀ (i : Fin n), -↑(d - 1) ≤ p ibound:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c i * ‖x + g i‖ ^ p ix:Space dh:0 ≤ ∑ i, c i * ‖x + g i‖ ^ p i⊢ ‖‖x‖ • f x‖ ≤ ‖‖x‖ * ∑ i, c i * ‖x + g i‖ ^ p i‖ F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhae:AEStronglyMeasurable (fun x => f x) volumen:ℕc:Fin n → ℝg:Fin n → Space dp:Fin n → ℤc_nonneg:∀ (i : Fin n), 0 ≤ c ip_bound:∀ (i : Fin n), -↑(d - 1) ≤ p ibound:∀ (x : Space d), ‖f x‖ ≤ ∑ i, c i * ‖x + g i‖ ^ p ix:Space dh:0 ≤ ∑ i, c i * ‖x + g i‖ ^ p i⊢ ‖x‖ * ‖f x‖ ≤ ‖x‖ * ∑ i, c i * ‖x + g i‖ ^ p i All goals completed! 🐙@[fun_prop] lemma norm_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded (fun x => ‖x‖ * f x) := hf.norm_smul_isDistBounded@[fun_prop] lemma component_smul_isDistBounded {d : ℕ} [NormedSpace ℝ F] {f : Space d → F} (hf : IsDistBounded f) (i : Fin d) : IsDistBounded (fun x => x i • f x) := F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fi:Fin d⊢ IsDistBounded fun x => x.val i • f x refine IsDistBounded.mono (f := fun x => ‖x‖ • f x) (F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fi:Fin d⊢ IsDistBounded fun x => ‖x‖ • f x All goals completed! 🐙) (AEStronglyMeasurable.smul ?_ (F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fi:Fin d⊢ AEStronglyMeasurable f volume All goals completed! 🐙)) fun x => ?_ F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fi:Fin d⊢ AEStronglyMeasurable (fun x => x.val i) volume simpa [coordCLM_apply, coord_apply] using (F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fi:Fin d⊢ AEStronglyMeasurable (fun x => (coordCLM i) x) volume All goals completed! 🐙 : AEStronglyMeasurable (fun x => Space.coordCLM i x)) F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fi:Fin dx:Space d⊢ ‖x.val i • f x‖ ≤ ‖‖x‖ • f x‖ F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fi:Fin dx:Space d⊢ |x.val i| * ‖f x‖ ≤ ‖x‖ * ‖f x‖ exact mul_le_mul_of_nonneg_right (abs_eval_le_norm x i) (F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fi:Fin dx:Space d⊢ 0 ≤ ‖f x‖ All goals completed! 🐙)@[fun_prop] lemma component_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (i : Fin d) : IsDistBounded (fun x => x i * f x) := hf.component_smul_isDistBounded i@[fun_prop] lemma isDistBounded_smul_self {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded (fun x => f x • x) := d:ℕf:Space d → ℝhf:IsDistBounded f⊢ IsDistBounded fun x => f x • x refine IsDistBounded.congr (f := fun x => ‖x‖ * f x) (d:ℕf:Space d → ℝhf:IsDistBounded f⊢ IsDistBounded fun x => ‖x‖ * f x All goals completed! 🐙) (AEStronglyMeasurable.smul (f := f) (g := fun x => x) (d:ℕf:Space d → ℝhf:IsDistBounded f⊢ AEStronglyMeasurable f volume All goals completed! 🐙) (d:ℕf:Space d → ℝhf:IsDistBounded f⊢ AEStronglyMeasurable (fun x => x) volume All goals completed! 🐙)) fun x => ?_ All goals completed! 🐙@[fun_prop] lemma isDistBounded_smul_self_repr {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded (fun x => f x • basis.repr x) := d:ℕf:Space d → ℝhf:IsDistBounded f⊢ IsDistBounded fun x => f x • basis.repr x refine IsDistBounded.congr (f := fun x => ‖x‖ * f x) (d:ℕf:Space d → ℝhf:IsDistBounded f⊢ IsDistBounded fun x => ‖x‖ * f x All goals completed! 🐙) (AEStronglyMeasurable.smul (f := f) (g := fun x => basis.repr x) (d:ℕf:Space d → ℝhf:IsDistBounded f⊢ AEStronglyMeasurable f volume All goals completed! 🐙) (d:ℕf:Space d → ℝhf:IsDistBounded f⊢ AEStronglyMeasurable (fun x => basis.repr x) volume All goals completed! 🐙)) fun x => ?_ All goals completed! 🐙F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fy:Space dh1:∀ (x : Space d), ⟪y, x⟫_ℝ • f x = ∑ i, (y.val i * x.val i) • f x⊢ IsDistBounded fun x => ⟪y, x⟫_ℝ • f x F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fy:Space dh1:∀ (x : Space d), ⟪y, x⟫_ℝ • f x = ∑ i, (y.val i * x.val i) • f x⊢ IsDistBounded fun x => ∑ x_1, y.val x_1 • x.val x_1 • f x exact sum_fun fun i _ => const_fun_smul (F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fy:Space dh1:∀ (x : Space d), ⟪y, x⟫_ℝ • f x = ∑ i, (y.val i * x.val i) • f xi:Fin dx✝:i ∈ Finset.univ⊢ IsDistBounded fun x => x.val i • f x All goals completed! 🐙) (y i)F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fun x => ‖x‖ • f xhae:AEStronglyMeasurable f volumey:Space dh1:∀ (x : Space d), ⟪y, x⟫_ℝ • f x = ∑ i, (y.val i * x.val i) • f x⊢ IsDistBounded fun x => ⟪y, x⟫_ℝ • f x F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fun x => ‖x‖ • f xhae:AEStronglyMeasurable f volumey:Space dh1:∀ (x : Space d), ⟪y, x⟫_ℝ • f x = ∑ i, (y.val i * x.val i) • f x⊢ IsDistBounded fun x => ∑ x_1, y.val x_1 • x.val x_1 • f x refine sum_fun fun i _ => const_fun_smul (hf.mono (F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fun x => ‖x‖ • f xhae:AEStronglyMeasurable f volumey:Space dh1:∀ (x : Space d), ⟪y, x⟫_ℝ • f x = ∑ i, (y.val i * x.val i) • f xi:Fin dx✝:i ∈ Finset.univ⊢ AEStronglyMeasurable (fun x => x.val i • f x) volume All goals completed! 🐙) fun x => ?_) (y i) F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fun x => ‖x‖ • f xhae:AEStronglyMeasurable f volumey:Space dh1:∀ (x : Space d), ⟪y, x⟫_ℝ • f x = ∑ i, (y.val i * x.val i) • f xi:Fin dx✝:i ∈ Finset.univx:Space d⊢ |x.val i| * ‖f x‖ ≤ ‖x‖ * ‖f x‖ exact mul_le_mul_of_nonneg_right (abs_eval_le_norm x i) (F:Typeinst✝¹:NormedAddCommGroup Fd:ℕinst✝:NormedSpace ℝ Ff:Space d → Fhf:IsDistBounded fun x => ‖x‖ • f xhae:AEStronglyMeasurable f volumey:Space dh1:∀ (x : Space d), ⟪y, x⟫_ℝ • f x = ∑ i, (y.val i * x.val i) • f xi:Fin dx✝:i ∈ Finset.univx:Space d⊢ 0 ≤ ‖f x‖ All goals completed! 🐙)@[fun_prop] lemma isDistBounded_mul_inner {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (y : Space d) : IsDistBounded (fun x => ⟪y, x⟫_ℝ * f x) := hf.isDistBounded_smul_inner ylemma isDistBounded_mul_inner' {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) (y : Space d) : IsDistBounded (fun x => ⟪x, y⟫_ℝ * f x) := d:ℕf:Space d → ℝhf:IsDistBounded fy:Space d⊢ IsDistBounded fun x => ⟪x, y⟫_ℝ * f x All goals completed! 🐙lemma isDistBounded_mul_inner_of_smul_norm {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded (fun x => ‖x‖ * f x)) (hae : AEStronglyMeasurable f) (y : Space d) : IsDistBounded (fun x => ⟪y, x⟫_ℝ * f x) := hf.isDistBounded_smul_inner_of_smul_norm hae y@[fun_prop] lemma mul_inner_pow_neg_two {d : ℕ} (y : Space d) (hd : 2 ≤ d := by omega) : IsDistBounded (fun x => ⟪y, x⟫_ℝ * ‖x‖ ^ (- 2 : ℤ)) := d:ℕy:Space dhd:2 ≤ d⊢ IsDistBounded fun x => ⟪y, x⟫_ℝ * ‖x‖ ^ (-2) refine IsDistBounded.mono (f := fun x => (‖y‖ * ‖x‖) * ‖x‖ ^ (- 2 : ℤ)) ?_ (AEMeasurable.aestronglyMeasurable (d:ℕy:Space dhd:2 ≤ d⊢ AEMeasurable (fun x => ⟪y, x⟫_ℝ * ‖x‖ ^ (-2)) volume All goals completed! 🐙)) fun x => ?_ d:ℕy:Space dhd:2 ≤ d⊢ IsDistBounded fun x => ‖y‖ * ‖x‖ * ‖x‖ ^ (-2) d:ℕy:Space dhd:2 ≤ d⊢ IsDistBounded fun x => ‖y‖ * (‖x‖ * ‖x‖ ^ (-2)) refine IsDistBounded.const_mul_fun (IsDistBounded.congr (f := fun x => ‖x‖ ^ (- 1 : ℤ)) (IsDistBounded.pow (d := d) (-1) (d:ℕy:Space dhd:2 ≤ d⊢ -↑(d - 1) ≤ -1 All goals completed! 🐙)) (AEMeasurable.aestronglyMeasurable (d:ℕy:Space dhd:2 ≤ d⊢ AEMeasurable (fun x => ‖x‖ * ‖x‖ ^ (-2)) volume All goals completed! 🐙)) fun x => ?_) ‖y‖ d:ℕy:Space dhd:2 ≤ dx:Space d⊢ ‖x‖ * (‖x‖ ^ 2)⁻¹ = ‖x‖⁻¹ d:ℕy:Space dhd:2 ≤ d⊢ ‖0‖ * (‖0‖ ^ 2)⁻¹ = ‖0‖⁻¹d:ℕy:Space dhd:2 ≤ dx:Space dhx:x ≠ 0⊢ ‖x‖ * (‖x‖ ^ 2)⁻¹ = ‖x‖⁻¹ d:ℕy:Space dhd:2 ≤ d⊢ ‖0‖ * (‖0‖ ^ 2)⁻¹ = ‖0‖⁻¹ All goals completed! 🐙 d:ℕy:Space dhd:2 ≤ dx:Space dhx:x ≠ 0⊢ ‖x‖ * (‖x‖ ^ 2)⁻¹ = ‖x‖⁻¹ All goals completed! 🐙 d:ℕy:Space dhd:2 ≤ dx:Space d⊢ ‖⟪y, x⟫_ℝ * ‖x‖ ^ (-2)‖ ≤ ‖‖y‖ * ‖x‖ * ‖x‖ ^ (-2)‖ d:ℕy:Space dhd:2 ≤ dx:Space d⊢ |⟪y, x⟫_ℝ| * (‖x‖ ^ 2)⁻¹ ≤ ‖y‖ * ‖x‖ * (‖x‖ ^ 2)⁻¹ exact mul_le_mul_of_nonneg (abs_real_inner_le_norm y x) (d:ℕy:Space dhd:2 ≤ dx:Space d⊢ (‖x‖ ^ 2)⁻¹ ≤ (‖x‖ ^ 2)⁻¹ All goals completed! 🐙) (d:ℕy:Space dhd:2 ≤ dx:Space d⊢ 0 ≤ |⟪y, x⟫_ℝ| All goals completed! 🐙) (d:ℕy:Space dhd:2 ≤ dx:Space d⊢ 0 ≤ (‖x‖ ^ 2)⁻¹ All goals completed! 🐙)