of_bounded — Mathlib

English

Under IsFiniteMeasure μ, if X(ω) ∈ Icc(a,b) a.e., HasFiniteIntegral X μ.

Русский

При IsFiniteMeasure μ, если X(ω) ∈ Icc(a,b) почти всюду, HasFiniteIntegral X μ.

LaTeX

$$$[IsFiniteMeasure\\mu] \\Rightarrow (\\forall^{\\mathrm{a}} \\omega, X(\\omega) \\in \\mathrm{Icc}(a,b)) \\Rightarrow HasFiniteIntegral X\\mu$$$

Lean4

theorem of_bounded [IsFiniteMeasure μ] {f : α → β} {C : ℝ} (hC : ∀ᵐ a ∂μ, ‖f a‖ ≤ C) : HasFiniteIntegral f μ :=
  (hasFiniteIntegral_const C).mono' hC

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