English
Suppose μ is σ-finite relative to m, and there exists a finite bound C on the μ-measure of all measurable sets s of finite μ-measure that satisfy μ(s) ≠ ∞, such that ∫‖f‖ ≤ C over s. Then f is integrable with respect to μ.
Русский
Пусть μ — σ-конечна относительно m, и существует конечная граница C такая, что на каждом измеримом множестве s с конечной мерой μ выполняется ∫‖f‖ ≤ C; тогда f интегрируемо по μ.
LaTeX
$$$ (hm: m \\le m_0) \\; (hf_int: \\operatorname{AEStronglyMeasurable} f \\mu)\\; (hf: ∀ s, \\mathrm{MeasurableSet}[m] s \\rightarrow \\mu s \\neq \\infty \\rightarrow \\int\\!\\!^{-} x \\in s, \\|f(x)\\|_\\varepsilon \\partial\\mu \\le C) \\Rightarrow \\operatorname{Integrable} f \\mu$$$
Lean4
theorem integrable_of_forall_fin_meas_le' {μ : Measure α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (C : ℝ≥0∞)
(hC : C < ∞) {f : α → ε} (hf_meas : AEStronglyMeasurable f μ)
(hf : ∀ s, MeasurableSet[m] s → μ s ≠ ∞ → ∫⁻ x in s, ‖f x‖ₑ ∂μ ≤ C) : Integrable f μ :=
⟨hf_meas, (lintegral_le_of_forall_fin_meas_trim_le hm C hf).trans_lt hC⟩
