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) : Prop

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 ⊤ μ
• measure_support_lt : μ (Function.support f) < ⊤

theorem BoundedFiniteSupport.aestronglyMeasurable {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [TopologicalSpace E] [ENorm E] [Zero E] {f : X → E} {μ : MeasureTheory.Measure X} (hf : BoundedFiniteSupport f μ) : MeasureTheory.AEStronglyMeasurable 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] [MeasurableSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [BorelSpace E] (bfs : BoundedFiniteSupport f μ) : 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] {s : Set X} (bfs : BoundedFiniteSupport f μ) : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)

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] [MeasurableSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [BorelSpace E] {s : Set X} (bfs : BoundedFiniteSupport f μ) : AEMeasurable f (μ.restrict s)

theorem BoundedFiniteSupport.measurable {X : Type u_1} {E : Type u_2} [MeasurableSpace X] {f : X → E} {μ : MeasureTheory.Measure X} [TopologicalSpace E] [ENorm E] [Zero E] [MeasurableSpace E] (bfs : BoundedFiniteSupport f μ) : Measurable f

theorem BoundedFiniteSupport.memLp {X : Type u_1} {E : Type u_2} [MeasurableSpace X] {f : X → E} {μ : MeasureTheory.Measure X} [NormedAddCommGroup 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 μ) : MeasureTheory.Integrable f μ

Bounded finitely supported functions are integrable.