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 μ) : 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] (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} : 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] (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 μ) : MeasureTheory.eLpNorm f ⊤ μ < ⊤

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

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) μ