structure
BoundedFiniteSupport
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
[TopologicalSpace E]
[ENorm E]
[Zero E]
(f : X → E)
(μ : MeasureTheory.Measure X := by volume_tac)
:
Definition to avoid repeating ourselves. Blueprint states: bounded measurable function $g$ on $X$ supported on a set of finite measure.
- memLp_top : MeasureTheory.MemLp f ⊤ μ
Instances For
theorem
BoundedFiniteSupport.aestronglyMeasurable
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[TopologicalSpace E]
[ENorm E]
[Zero E]
(bfs : BoundedFiniteSupport f μ)
:
theorem
BoundedFiniteSupport.aemeasurable
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[TopologicalSpace E]
[ENorm E]
[Zero E]
(bfs : BoundedFiniteSupport f μ)
[MeasurableSpace E]
[TopologicalSpace.PseudoMetrizableSpace E]
[BorelSpace E]
:
AEMeasurable f μ
theorem
BoundedFiniteSupport.aestronglyMeasurable_restrict
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[TopologicalSpace E]
[ENorm E]
[Zero E]
(bfs : BoundedFiniteSupport f μ)
{s : Set X}
:
theorem
BoundedFiniteSupport.aemeasurable_restrict
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[TopologicalSpace E]
[ENorm E]
[Zero E]
(bfs : BoundedFiniteSupport f μ)
[MeasurableSpace E]
[TopologicalSpace.PseudoMetrizableSpace E]
[BorelSpace E]
{s : Set X}
:
AEMeasurable f (μ.restrict s)
theorem
BoundedFiniteSupport.eLpNorm_lt_top
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[TopologicalSpace E]
[ENorm E]
[Zero E]
(bfs : BoundedFiniteSupport f μ)
:
theorem
BoundedFiniteSupport.memLp
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[TopologicalSpace E]
[ENormedAddMonoid E]
(hf : BoundedFiniteSupport f μ)
(p : ENNReal)
:
MeasureTheory.MemLp f p μ
Bounded finitely supported functions are in all Lᵖ spaces.
theorem
BoundedFiniteSupport.integrable
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
(hf : BoundedFiniteSupport f μ)
:
Bounded finitely supported functions are integrable.
theorem
BoundedFiniteSupport.indicator
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
(bfs : BoundedFiniteSupport f μ)
{s : Set X}
(hs : MeasurableSet s)
:
BoundedFiniteSupport (s.indicator f) μ
theorem
BoundedFiniteSupport.neg
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f : X → E}
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
(hf : BoundedFiniteSupport f μ)
:
BoundedFiniteSupport (-f) μ
theorem
BoundedFiniteSupport.add
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f g : X → E}
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
(hf : BoundedFiniteSupport f μ)
(hg : BoundedFiniteSupport g μ)
:
BoundedFiniteSupport (f + g) μ
theorem
BoundedFiniteSupport.sub
{X : Type u_1}
{E : Type u_2}
[MeasurableSpace X]
{f g : X → E}
{μ : MeasureTheory.Measure X}
[NormedAddCommGroup E]
(hf : BoundedFiniteSupport f μ)
(hg : BoundedFiniteSupport g μ)
:
BoundedFiniteSupport (f - g) μ