LeanPool.RlTheoryInLean.MeasureTheory.Function.L1Space.Integrable #
theorem
MeasureTheory.integrable_of_norm_le
{α : Type u_2}
{β : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
[NormedAddCommGroup β]
{f : α → β}
(hm : AEStronglyMeasurable f μ)
(hbdd : ∃ (C : ℝ), ∀ᵐ (ω : α) ∂μ, ‖f ω‖ ≤ C)
:
Integrable f μ
theorem
MeasureTheory.Integrable.finset_sum
{α : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{s : Finset ι}
{f : ι → α → ℝ}
(hf : ∀ i ∈ s, Integrable (f i) μ)
:
Integrable (fun (ω : α) => ∑ i ∈ s, f i ω) μ