English
If μ is σ-finite and the same finite-measure bound condition holds for all measurable sets s with μ(s) ≠ ∞, then f is integrable with respect to μ.
Русский
Если μ является σ-конечной, и выполняется условие конечной меры для всех измеримых множеств s с μ(s) ≠ ∞, то f интегрируемо по μ.
LaTeX
$$$ (hm: m \\le m_0) [\\operatorname{SigmaFinite} \\mu] (C: \\mathbb{R}_{\\ge 0}^{\\infty}) (hC: C < \\infty) {f: α \\to ε} (hf_meas: \\operatorname{AEStronglyMeasurable}_m f \\mu) (hf: \\forall s, \\operatorname{MeasurableSet}[m] s \\rightarrow \\mu s \\neq \\infty \\rightarrow \\int^{\\infty}_{x\\in s} \\|f(x)\\|_e \\partial\\mu \\le C) : \\operatorname{Integrable} f \\mu$$
Lean4
theorem integrable_of_forall_fin_meas_le [SigmaFinite μ] (C : ℝ≥0∞) (hC : C < ∞) {f : α → ε}
(hf_meas : AEStronglyMeasurable[m] f μ)
(hf : ∀ s : Set α, MeasurableSet[m] s → μ s ≠ ∞ → ∫⁻ x in s, ‖f x‖ₑ ∂μ ≤ C) : Integrable f μ :=
have : SigmaFinite (μ.trim le_rfl) := by rwa [@trim_eq_self _ m]
integrable_of_forall_fin_meas_le' le_rfl C hC hf_meas hf
