integrableOn_of_bounded — Mathlib

English

FiniteAtFilter integrability results give: if f tends to b along l, then IntegrableAtFilter f l μ.

Русский

Если f сходится к границе по l, то f интегрируемо по l.

LaTeX

$$$\\operatorname{integrableAtFilter\_of\_tendsto}(f, l, \\mu) : \\operatorname{IntegrableAtFilter}(f, l, \\mu).$$$

Lean4

theorem integrableOn_of_bounded {f : α → E} (s_finite : μ s ≠ ∞) (f_mble : AEStronglyMeasurable f μ) {M : ℝ}
    (f_bdd : ∀ᵐ a ∂(μ.restrict s), ‖f a‖ ≤ M) : IntegrableOn f s μ :=
  ⟨f_mble.restrict, .restrict_of_bounded (C := M) s_finite.lt_top f_bdd⟩

Похожие утверждения