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
Upstreaming status: should be upstreamed, but need to clarify design questions first
- want to tag this with fun_prop first and make it work smoothly (see #499)
- this is similar to
BoundedFiniteSupport(and in almost all cases, implies the latter) TODO: are there any advantages of using this and not BoundedFiniteSupport? for instance, is there any operation which preservesBoundedCompactSupportbut notBoundedFiniteSupport? Decide if we want both classes in mathlib or just one of them. If the latter, rewrite all of Carleson/ToMathlib to use that one class.
theorem
MeasureTheory.eLpNorm_mono_ac
{α : Type u_3}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hμν : ν.AbsolutelyContinuous μ)
:
theorem
MeasureTheory.MemLp.mono_ac
{α : Type u_3}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ContinuousENorm ε]
{f : α → ε}
(hf : MemLp f ⊤ μ)
(hμν : ν.AbsolutelyContinuous μ)
:
theorem
MeasureTheory.MemLp.comp_quasiMeasurePreserving
{α : Type u_3}
{m0 : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_4}
[TopologicalSpace ε]
[ContinuousENorm ε]
{β : Type u_5}
{mβ : MeasurableSpace β}
{f : α → β}
{g : β → ε}
{ν : Measure β}
(hg : MemLp g ⊤ ν)
(hf : Measure.QuasiMeasurePreserving f μ ν)
:
structure
MeasureTheory.BoundedCompactSupport
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
[TopologicalSpace E]
[ENorm E]
[Zero E]
(f : X → E)
(μ : Measure X := by volume_tac)
:
Bounded compactly supported measurable functions
- hasCompactSupport : HasCompactSupport f
Instances For
theorem
isBounded_range_iff_forall_norm_le
{α : Type u_3}
{β : Sort u_4}
[SeminormedAddCommGroup α]
{f : β → α}
:
theorem
MeasureTheory.BoundedCompactSupport.aestronglyMeasurable
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[TopologicalSpace E]
[ENorm E]
[Zero E]
(hf : BoundedCompactSupport f μ)
:
theorem
MeasureTheory.BoundedCompactSupport.boundedFiniteSupport
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[TopologicalSpace E]
[ENorm E]
[Zero E]
[IsFiniteMeasureOnCompacts μ]
(hf : BoundedCompactSupport f μ)
:
theorem
MeasureTheory.BoundedCompactSupport.mono_ac
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ ν : Measure X}
{f : X → E}
[TopologicalSpace E]
[ContinuousENorm E]
[Zero E]
(hf : BoundedCompactSupport f μ)
(h : ν.AbsolutelyContinuous μ)
:
theorem
MeasureTheory.BoundedCompactSupport.mono_measure
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ ν : Measure X}
{f : X → E}
[TopologicalSpace E]
[ContinuousENorm E]
[Zero E]
(hf : BoundedCompactSupport f μ)
(h : ν ≤ μ)
:
theorem
MeasureTheory.BoundedCompactSupport.restrict
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[TopologicalSpace E]
[ContinuousENorm E]
[Zero E]
{s : Set X}
(hf : BoundedCompactSupport f μ)
:
BoundedCompactSupport f (μ.restrict s)
theorem
MeasureTheory.BoundedCompactSupport.memLp
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[TopologicalSpace E]
[ENormedAddCommMonoid E]
[IsFiniteMeasureOnCompacts μ]
(hf : BoundedCompactSupport f μ)
(p : ENNReal)
:
MemLp f p μ
Bounded compactly supported functions are in all Lᵖ spaces.
theorem
MeasureTheory.BoundedCompactSupport.integrable
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
[IsFiniteMeasureOnCompacts μ]
(hf : BoundedCompactSupport f μ)
:
Integrable f μ
Bounded compactly supported functions are integrable.
theorem
MeasureTheory.BoundedCompactSupport.zero
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
[NormedAddCommGroup E]
:
BoundedCompactSupport (fun (x : X) => 0) μ
theorem
MeasureTheory.BoundedCompactSupport.enorm
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
(hf : BoundedCompactSupport f μ)
:
BoundedCompactSupport (fun (x : X) => ‖f x‖ₑ) μ
theorem
MeasureTheory.BoundedCompactSupport.norm
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
(hf : BoundedCompactSupport f μ)
:
BoundedCompactSupport (fun (x : X) => ‖f x‖) μ
theorem
MeasureTheory.BoundedCompactSupport.comp_left_norm
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
{F : Type u_3}
[NormedAddCommGroup F]
{g : E → F}
(hf : BoundedCompactSupport f μ)
(hg : g 0 = 0)
(hg1 : Continuous g)
(hg2 : ∀ (a : E), ‖g a‖ = ‖a‖)
:
BoundedCompactSupport (g ∘ f) μ
theorem
MeasureTheory.BoundedCompactSupport.neg
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
(hf : BoundedCompactSupport f μ)
:
BoundedCompactSupport (-f) μ
theorem
MeasureTheory.BoundedCompactSupport.add
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
{g : X → E}
(hf : BoundedCompactSupport f μ)
(hg : BoundedCompactSupport g μ)
:
BoundedCompactSupport (f + g) μ
theorem
MeasureTheory.BoundedCompactSupport.sub
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
{g : X → E}
(hf : BoundedCompactSupport f μ)
(hg : BoundedCompactSupport g μ)
:
BoundedCompactSupport (f - g) μ
theorem
MeasureTheory.BoundedCompactSupport.mul_bdd_right
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f g : X → 𝕜}
(hf : BoundedCompactSupport f μ)
(hg : MemLp g ⊤ μ)
:
BoundedCompactSupport (f * g) μ
theorem
MeasureTheory.BoundedCompactSupport.mul_bdd_left
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f g : X → 𝕜}
(hf : BoundedCompactSupport f μ)
(hg : MemLp g ⊤ μ)
:
BoundedCompactSupport (g * f) μ
theorem
MeasureTheory.BoundedCompactSupport.mul
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f g : X → 𝕜}
(hf : BoundedCompactSupport f μ)
(hg : BoundedCompactSupport g μ)
:
BoundedCompactSupport (f * g) μ
theorem
MeasureTheory.BoundedCompactSupport.integrable_mul
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f g : X → 𝕜}
(hf : BoundedCompactSupport f μ)
(hg : Integrable g μ)
:
Integrable (f * g) μ
theorem
MeasureTheory.BoundedCompactSupport.integrable_fun_mul
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f g : X → 𝕜}
(hf : BoundedCompactSupport f μ)
(hg : Integrable g μ)
:
Integrable (fun (x : X) => f x * g x) μ
theorem
HasCompactSupport.star
{X : Type u_1}
[TopologicalSpace X]
{𝕜 : Type u_3}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : HasCompactSupport f)
:
HasCompactSupport fun (i : X) => Star.star (f i)
theorem
AEStronglyMeasurable.star
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.BoundedCompactSupport.conj
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : BoundedCompactSupport f μ)
:
BoundedCompactSupport (star f) μ
theorem
MeasureTheory.BoundedCompactSupport.starRingEnd
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : BoundedCompactSupport f μ)
:
BoundedCompactSupport (fun (x : X) => (_root_.starRingEnd 𝕜) (f x)) μ
theorem
MeasureTheory.BoundedCompactSupport.const_mul
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : BoundedCompactSupport f μ)
(c : 𝕜)
:
BoundedCompactSupport (fun (x : X) => c * f x) μ
theorem
MeasureTheory.BoundedCompactSupport.mul_const
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : BoundedCompactSupport f μ)
(c : 𝕜)
:
BoundedCompactSupport (fun (x : X) => f x * c) μ
theorem
MeasureTheory.BoundedCompactSupport.mono
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
{g : X → ENNReal}
(hg : BoundedCompactSupport g μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ (x : X), ‖f x‖ₑ ≤ g x)
:
If ‖f‖ is bounded by g and g is bounded compactly supported, then so is f.
theorem
MeasureTheory.BoundedCompactSupport.mono_norm
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → E}
[NormedAddCommGroup E]
{g : X → ℝ}
(hg : BoundedCompactSupport g μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ (x : X), ‖f x‖ ≤ g x)
:
theorem
MeasureTheory.BoundedCompactSupport.toComplex
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{f : X → ℝ}
(hf : BoundedCompactSupport f μ)
:
BoundedCompactSupport (fun (x : X) => ↑(f x)) μ
theorem
MeasureTheory.BoundedCompactSupport.finset_sum
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
[NormedAddCommGroup E]
{ι : Type u_4}
{s : Finset ι}
{F : ι → X → E}
(hF : ∀ i ∈ s, BoundedCompactSupport (F i) μ)
:
BoundedCompactSupport (fun (x : X) => ∑ i ∈ s, F i x) μ
A finite sum of bounded compactly supported functions is bounded compactly supported.
theorem
MeasureTheory.BoundedCompactSupport.sq_eLpNorm_le_sums
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{ι : Type u_4}
[IsFiniteMeasureOnCompacts μ]
{f : ι → X → ℂ}
(hf : ∀ (i : ι), BoundedCompactSupport (f i) μ)
{s : Finset ι}
:
Used in Proposition 2.0.4.
theorem
MeasureTheory.BoundedCompactSupport.prod_mul
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
{𝕜 : Type u_3}
[RCLike 𝕜]
{Y : Type u_4}
[MeasureSpace Y]
{f : X → 𝕜}
{g : Y → 𝕜}
{ν : Measure Y}
[TopologicalSpace Y]
[R1Space (X × Y)]
(hf : BoundedCompactSupport f μ)
(hg : BoundedCompactSupport g ν)
:
BoundedCompactSupport (Function.uncurry fun (x : X) (y : Y) => f x * g y) (μ.prod ν)
An elementary tensor of bounded compactly supported functions is bounded compactly supported.
theorem
MeasureTheory.BoundedCompactSupport.indicator_of_isCompact_closure
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
[NormedAddCommGroup E]
[R1Space X]
{f : X → E}
(hf : MemLp f ⊤ μ)
{s : Set X}
(h's : IsCompact (closure s))
(hs : MeasurableSet s)
:
BoundedCompactSupport (s.indicator f) μ
theorem
MeasureTheory.BoundedCompactSupport.indicator
{X : Type u_1}
{E : Type u_2}
[TopologicalSpace X]
[MeasurableSpace X]
{μ : Measure X}
[NormedAddCommGroup E]
{f : X → E}
(hf : BoundedCompactSupport f μ)
{s : Set X}
(hs : MeasurableSet s)
:
BoundedCompactSupport (s.indicator f) μ
theorem
MeasureTheory.BoundedCompactSupport.isBoundedTSupport
{X : Type u_1}
{E : Type u_2}
[MetricSpace X]
[MeasurableSpace X]
{μ : Measure X}
[TopologicalSpace E]
[ENorm E]
[Zero E]
{f : X → E}
(hf : BoundedCompactSupport f μ)
:
theorem
MeasureTheory.BoundedCompactSupport.isBoundedSupport
{X : Type u_1}
{E : Type u_2}
[MetricSpace X]
[MeasurableSpace X]
{μ : Measure X}
[TopologicalSpace E]
[ENorm E]
[Zero E]
{f : X → E}
(hf : BoundedCompactSupport f μ)
:
theorem
BoundedCompactSupport.mul_bdd_right''
{X : Type u_1}
{𝕜 : Type u_2}
[MeasurableSpace X]
[MetricSpace X]
{W : Type u_6}
[MeasurableSpace W]
[TopologicalSpace W]
{μ : MeasureTheory.Measure W}
{f : X → 𝕜}
{ν : MeasureTheory.Measure X}
[RCLike 𝕜]
(hf : MeasureTheory.BoundedCompactSupport f ν)
{e : W → X}
{g : W → 𝕜}
(he : Continuous e)
(he1 : MeasureTheory.Measure.QuasiMeasurePreserving e μ ν)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hg1 : ∀ (K : Set X), IsCompact K → IsCompact (e ⁻¹' K ∩ tsupport g))
(hg2 : ∀ (A : Set X), Bornology.IsBounded A → Bornology.IsBounded (g '' (e ⁻¹' A)))
:
MeasureTheory.BoundedCompactSupport (fun (x : W) => f (e x) * g x) μ
theorem
BoundedCompactSupport.mul_bdd_left'
{X : Type u_1}
{𝕜 : Type u_2}
[MeasurableSpace X]
[MetricSpace X]
{W : Type u_6}
[MeasurableSpace W]
[TopologicalSpace W]
{μ : MeasureTheory.Measure W}
{f : X → 𝕜}
{ν : MeasureTheory.Measure X}
[RCLike 𝕜]
(hf : MeasureTheory.BoundedCompactSupport f ν)
{e : W → X}
{g : W → 𝕜}
(he : Continuous e)
(he1 : MeasureTheory.Measure.QuasiMeasurePreserving e μ ν)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hg1 : ∀ (K : Set X), IsCompact K → IsCompact (e ⁻¹' K ∩ tsupport g))
(hg2 : ∀ (A : Set X), Bornology.IsBounded A → Bornology.IsBounded (g '' (e ⁻¹' A)))
:
MeasureTheory.BoundedCompactSupport (fun (x : W) => g x * f (e x)) μ