of_bound — Mathlib

English

If μ is finite and f is AEStronglyMeasurable and essentially bounded by C, then f is integrable with respect to μ.

Русский

Если μ получима конечной мерой, и f измерима и по существу ограничена константой C, то f интегрируема по μ.

LaTeX

$$$[IsFiniteMeasure\;\mu] \Rightarrow \mathrm{AEStronglyMeasurable}(f,\mu) \to (\forall\,C\in\mathbb{R}, \forall^{\ast} x\,\partial\mu, \|f(x)\| \le C) \to \mathrm{Integrable}(f,\mu)$$$

Lean4

theorem of_bound [IsFiniteMeasure μ] {f : α → E} (hf : AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
    Integrable f μ :=
  ⟨hf, .of_bounded hfC⟩

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