Documentation

Carleson.ToMathlib.BoundedCompactSupport

EXPERIMENTAL

Bounded compactly supported functions #

The purpose of this file is to provide helper lemmas to streamline proofs that functions are (essentially) bounded, compactly supported and measurable.

Most functions we need to deal with are of this class. This can be a useful way to streamline proofs of L^p membership, in particular integrability.

Todo: make Mathlib.Tactic.FunProp work for this

This can be expanded as needed

source
structure MeasureTheory.BoundedCompactSupport {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] (f : X β†’ π•œ) [TopologicalSpace X] :
Prop

Bounded compactly supported measurable functions

Instances For
    source
    theorem MeasureTheory.isBounded_range_iff_forall_norm_le {Ξ± : Type u_1} {Ξ² : Sort u_2} [SeminormedAddCommGroup Ξ±] {f : Ξ² β†’ Ξ±} :
    Bornology.IsBounded (Set.range f) ↔ βˆƒ (C : ℝ), βˆ€ (x : Ξ²), β€–f xβ€– ≀ C
    source
    theorem Bornology.IsBounded.eLpNorm_top_lt_top {X : Type u_2} {π•œ : Type u_1} [MeasureTheory.MeasureSpace X] [RCLike π•œ] {f : X β†’ π•œ} [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] (hf : Bornology.IsBounded (Set.range f)) :
    MeasureTheory.eLpNorm f ⊀ MeasureTheory.volume < ⊀
    source
    theorem MeasureTheory.BoundedCompactSupport.mk' {X : Type u_2} {π•œ : Type u_1} [MeasureTheory.MeasureSpace X] [RCLike π•œ] {f : X β†’ π•œ} [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] (hf : Bornology.IsBounded (Set.range f)) (h2f : HasCompactSupport f) (h3f : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
    MeasureTheory.BoundedCompactSupport f
    source
    theorem MeasureTheory.ae_le_of_eLpNorm_top_lt_top {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] {f : X β†’ π•œ} [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] (hf : MeasureTheory.eLpNorm f ⊀ MeasureTheory.volume < ⊀) :
    βˆ€α΅ (x : X), β€–f xβ€– ≀ (MeasureTheory.eLpNorm f ⊀ MeasureTheory.volume).toReal
    source
    theorem MeasureTheory.BoundedCompactSupport.aestronglyMeasurable {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) :
    MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume
    source
    theorem MeasureTheory.BoundedCompactSupport.ae_le {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) :
    βˆ€α΅ (x : X), β€–f xβ€– ≀ (MeasureTheory.eLpNorm f ⊀ MeasureTheory.volume).toReal
    source
    theorem MeasureTheory.BoundedCompactSupport.memβ„’p {X : Type u_2} {π•œ : Type u_1} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (p : ENNReal) :
    MeasureTheory.Memβ„’p f p MeasureTheory.volume

    Bounded compactly supported functions are in all Lα΅– spaces.

    source
    theorem MeasureTheory.BoundedCompactSupport.integrable {X : Type u_2} {π•œ : Type u_1} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) :
    MeasureTheory.Integrable f MeasureTheory.volume

    Bounded compactly supported functions are integrable.

    source
    theorem MeasureTheory.BoundedCompactSupport.mul_ess_bdd_right {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f g : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (hg : MeasureTheory.eLpNorm g ⊀ MeasureTheory.volume < ⊀) (h2g : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) :
    MeasureTheory.BoundedCompactSupport (f * g)
    source
    theorem MeasureTheory.BoundedCompactSupport.mul_ess_bdd_left {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f g : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (hg : MeasureTheory.eLpNorm g ⊀ MeasureTheory.volume < ⊀) (h2g : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) :
    MeasureTheory.BoundedCompactSupport (g * f)
    source
    theorem MeasureTheory.BoundedCompactSupport.mul_bdd_right {X : Type u_2} {π•œ : Type u_1} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f g : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (hg : Bornology.IsBounded (Set.range g)) (h2g : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) :
    MeasureTheory.BoundedCompactSupport (f * g)

    A bounded compactly supported function times a bounded function is bounded compactly supported.

    source
    theorem MeasureTheory.BoundedCompactSupport.mul_bdd_left {X : Type u_2} {π•œ : Type u_1} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f g : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (hg : Bornology.IsBounded (Set.range g)) (h2g : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) :
    MeasureTheory.BoundedCompactSupport (g * f)
    source
    theorem MeasureTheory.BoundedCompactSupport.integrable_mul {X : Type u_2} {π•œ : Type u_1} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f g : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (hg : MeasureTheory.Integrable g MeasureTheory.volume) :
    MeasureTheory.Integrable (f * g) MeasureTheory.volume
    source
    theorem MeasureTheory.BoundedCompactSupport.conj {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) :
    MeasureTheory.BoundedCompactSupport (star f)
    source
    theorem MeasureTheory.BoundedCompactSupport.norm {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) :
    MeasureTheory.BoundedCompactSupport fun (x : X) => β€–f xβ€–
    source
    theorem MeasureTheory.BoundedCompactSupport.const_mul {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (c : π•œ) :
    MeasureTheory.BoundedCompactSupport fun (x : X) => c * f x
    source
    theorem MeasureTheory.BoundedCompactSupport.mul_const {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (c : π•œ) :
    MeasureTheory.BoundedCompactSupport fun (x : X) => f x * c
    source
    theorem MeasureTheory.BoundedCompactSupport.mul {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f g : X β†’ π•œ} (hf : MeasureTheory.BoundedCompactSupport f) (hg : MeasureTheory.BoundedCompactSupport g) :
    MeasureTheory.BoundedCompactSupport (f * g)
    source
    theorem MeasureTheory.BoundedCompactSupport.mono {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} {g : X β†’ ℝ} (hg : MeasureTheory.BoundedCompactSupport g) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hfg : βˆ€ (x : X), β€–f xβ€– ≀ g x) :
    MeasureTheory.BoundedCompactSupport f

    If β€–fβ€– is bounded by g and g is bounded compactly supported, then so is f.

    source
    theorem MeasureTheory.BoundedCompactSupport.of_norm_le_const_mul {X : Type u_1} {π•œ : Type u_2} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {f : X β†’ π•œ} [T2Space X] {g : X β†’ ℝ} {M : ℝ} (hg : MeasureTheory.BoundedCompactSupport g) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hfg : βˆ€ (x : X), β€–f xβ€– ≀ M * g x) :
    MeasureTheory.BoundedCompactSupport f
    source
    theorem MeasureTheory.BoundedCompactSupport.finset_sum {X : Type u_2} {π•œ : Type u_3} [MeasureTheory.MeasureSpace X] [RCLike π•œ] [TopologicalSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {ΞΉ : Type u_1} {s : Finset ΞΉ} {F : ΞΉ β†’ X β†’ π•œ} (hF : βˆ€ i ∈ s, MeasureTheory.BoundedCompactSupport (F i)) :
    MeasureTheory.BoundedCompactSupport fun (x : X) => βˆ‘ i ∈ s, F i x

    A finite sum of bounded compactly supported functions is bounded compactly supported.

    source
    theorem MeasureTheory.BoundedCompactSupport.isBoundedSupport' {X : Type u_1} {π•œ : Type u_3} [RCLike π•œ] [MeasureTheory.MeasureSpace X] {f : X β†’ π•œ} [PseudoMetricSpace X] [MeasureTheory.SigmaFinite MeasureTheory.volume] (hf : MeasureTheory.BoundedCompactSupport f) :
    Bornology.IsBounded (tsupport f)
    source
    theorem MeasureTheory.BoundedCompactSupport.isBoundedSupport {X : Type u_1} {π•œ : Type u_3} [RCLike π•œ] [MeasureTheory.MeasureSpace X] {f : X β†’ π•œ} [PseudoMetricSpace X] [MeasureTheory.SigmaFinite MeasureTheory.volume] (hf : MeasureTheory.BoundedCompactSupport f) :
    Bornology.IsBounded (Function.support f)