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 dAEStronglyMeasurable (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 fAEMeasurable (fun x => ((1 + x) ^ r)⁻¹) volume All goals completed! 🐙)) (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace Fd:r:f:Space d Fhf:IsDistBounded fAEStronglyMeasurable 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 × D20 ((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 × D20 ((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 × D20 < (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 × D20 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 × D21 + 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 × D20 < (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 × D20 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 × D21 + 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 dx.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 d0 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 gIsDistBounded (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 iIsDistBounded (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 iIsDistBounded (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 iAEStronglyMeasurable (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 n10 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 n20 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 gIsDistBounded 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 iIsDistBounded (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 iAEStronglyMeasurable (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 dc * 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 fIsDistBounded 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 nIsDistBounded 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 iIsDistBounded 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 iAEStronglyMeasurable (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 nIsDistBounded 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 iIsDistBounded 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 iAEStronglyMeasurable (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 xIsDistBounded 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 xhae1: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 iIsDistBounded 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 xIsDistBounded 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 xhae1: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 iIsDistBounded 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 iIsDistBounded 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 iAEStronglyMeasurable (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 df 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:FAEStronglyMeasurable (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 dc 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:FAEStronglyMeasurable (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) nAEMeasurable (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) nAEMeasurable (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 dIsDistBounded 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 < aIsDistBounded 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 d0 < a ^ (n + 1) All goals completed! 🐙) (pow_le_pow_left₀ ha.le (d:n✝:a:ha:0 < an:x:Space da 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 dIsDistBounded 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 dIsDistBounded 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 dIsDistBounded 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 xh2:Real.log x xReal.log x x⁻¹ + x -Real.log x x⁻¹ + x d:hd:2 dx:Space dh1:-x⁻¹ Real.log xh2:Real.log x xReal.log x x⁻¹ + xd:hd:2 dx:Space dh1:-x⁻¹ Real.log xh2:Real.log x x-Real.log x x⁻¹ + x d:hd:2 dx:Space dh1:-x⁻¹ Real.log xh2:Real.log x xReal.log x x⁻¹ + x exact h2.trans (d:hd:2 dx:Space dh1:-x⁻¹ Real.log xh2:Real.log x xx x⁻¹ + x All goals completed! 🐙) d:hd:2 dx:Space dh1:-x⁻¹ Real.log xh2: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 nIsDistBounded fun x => x ^ n x d:n:hn:-(d - 1) - 1 nhzero:n = -1IsDistBounded fun x => x ^ n xd:n:hn:-(d - 1) - 1 nhzero:¬n = -1IsDistBounded fun x => x ^ n x d:n:hn:-(d - 1) - 1 nhzero:n = -1IsDistBounded fun x => x ^ n x d:hn:-(d - 1) - 1 -1IsDistBounded fun x => x ^ (-1) x refine IsDistBounded.mono (f := fun x => (1 : )) (d:hn:-(d - 1) - 1 -1IsDistBounded fun x => 1 All goals completed! 🐙) (AEMeasurable.aestronglyMeasurable (d:hn:-(d - 1) - 1 -1AEMeasurable (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 = -1AEMeasurable (fun x => x ^ n x) volume All goals completed! 🐙)) fun x => ?_ d:n:hn:-(d - 1) - 1 nhzero:¬n = -10 ^ n 0 = 0 ^ (n + 1)d:n:hn:-(d - 1) - 1 nhzero:¬n = -1x:Space dhx:x 0x ^ n x = x ^ (n + 1) d:n:hn:-(d - 1) - 1 nhzero:¬n = -10 ^ n 0 = 0 ^ (n + 1) All goals completed! 🐙 d:n:hn:-(d - 1) - 1 nhzero:¬n = -1x:Space dhx:x 0x ^ 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 nAEMeasurable (fun x => x ^ n basis.repr x) volume All goals completed! 🐙)) fun x => d:n:hn:-(d - 1) - 1 nx:Space dx ^ 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 -nIsDistBounded 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 -nIsDistBounded 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 dx * x + c ^ p x * (x + c) ^ p d:p:c:Space dx:Space dx + c x + c All goals completed! 🐙d:p✝:c:Space dp:hn:-(d - 1) Int.negSucc php:¬p = 0x:Space dx * (x ^ (p + 1))⁻¹ = (x ^ p)⁻¹ d:p✝:c:Space dp:hn:-(d - 1) Int.negSucc php:¬p = 0x:Space dhx:x = 0x * (x ^ (p + 1))⁻¹ = (x ^ p)⁻¹d:p✝:c:Space dp:hn:-(d - 1) Int.negSucc php:¬p = 0x:Space dhx:x 0x * (x ^ (p + 1))⁻¹ = (x ^ p)⁻¹ d:p✝:c:Space dp:hn:-(d - 1) Int.negSucc php:¬p = 0x:Space dhx:x = 0x * (x ^ (p + 1))⁻¹ = (x ^ p)⁻¹ All goals completed! 🐙 d:p✝:c:Space dp:hn:-(d - 1) Int.negSucc php:¬p = 0x:Space dhx:x 0x * (x ^ (p + 1))⁻¹ = (x ^ p)⁻¹ d:p✝:c:Space dp:hn:-(d - 1) Int.negSucc php:¬p = 0x:Space dhx:x 0x * 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 ix 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 ix * 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 dIsDistBounded 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 dIsDistBounded fun x => x f x All goals completed! 🐙) (AEStronglyMeasurable.smul ?_ (F:Typeinst✝¹:NormedAddCommGroup Fd:inst✝:NormedSpace Ff:Space d Fhf:IsDistBounded fi:Fin dAEStronglyMeasurable f volume All goals completed! 🐙)) fun x => ?_ F:Typeinst✝¹:NormedAddCommGroup Fd:inst✝:NormedSpace Ff:Space d Fhf:IsDistBounded fi:Fin dAEStronglyMeasurable (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 dAEStronglyMeasurable (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 dx.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 d0 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 fIsDistBounded fun x => f x x refine IsDistBounded.congr (f := fun x => x * f x) (d:f:Space d hf:IsDistBounded fIsDistBounded fun x => x * f x All goals completed! 🐙) (AEStronglyMeasurable.smul (f := f) (g := fun x => x) (d:f:Space d hf:IsDistBounded fAEStronglyMeasurable f volume All goals completed! 🐙) (d:f:Space d hf:IsDistBounded fAEStronglyMeasurable (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 fIsDistBounded fun x => f x basis.repr x refine IsDistBounded.congr (f := fun x => x * f x) (d:f:Space d hf:IsDistBounded fIsDistBounded fun x => x * f x All goals completed! 🐙) (AEStronglyMeasurable.smul (f := f) (g := fun x => basis.repr x) (d:f:Space d hf:IsDistBounded fAEStronglyMeasurable f volume All goals completed! 🐙) (d:f:Space d hf:IsDistBounded fAEStronglyMeasurable (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 xIsDistBounded 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 xIsDistBounded 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.univIsDistBounded 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 xIsDistBounded 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 xIsDistBounded 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.univAEStronglyMeasurable (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 d0 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 dIsDistBounded 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 dIsDistBounded fun x => y, x⟫_ * x ^ (-2) refine IsDistBounded.mono (f := fun x => (y * x) * x ^ (- 2 : )) ?_ (AEMeasurable.aestronglyMeasurable (d:y:Space dhd:2 dAEMeasurable (fun x => y, x⟫_ * x ^ (-2)) volume All goals completed! 🐙)) fun x => ?_ d:y:Space dhd:2 dIsDistBounded fun x => y * x * x ^ (-2) d:y:Space dhd:2 dIsDistBounded 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 dAEMeasurable (fun x => x * x ^ (-2)) volume All goals completed! 🐙)) fun x => ?_) y d:y:Space dhd:2 dx:Space dx * (x ^ 2)⁻¹ = x⁻¹ d:y:Space dhd:2 d0 * (0 ^ 2)⁻¹ = 0⁻¹d:y:Space dhd:2 dx:Space dhx:x 0x * (x ^ 2)⁻¹ = x⁻¹ d:y:Space dhd:2 d0 * (0 ^ 2)⁻¹ = 0⁻¹ All goals completed! 🐙 d:y:Space dhd:2 dx:Space dhx:x 0x * (x ^ 2)⁻¹ = x⁻¹ All goals completed! 🐙 d:y:Space dhd:2 dx:Space dy, 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 d0 |y, x⟫_| All goals completed! 🐙) (d:y:Space dhd:2 dx:Space d0 (x ^ 2)⁻¹ All goals completed! 🐙)