of_mem_Icc_enorm — Mathlib

English

If X is AEStronglyMeasurable, takes values in [a,b] a.e., and μ is finite, then X is integrable whenever a,b are finite and X is a.e. bounded.

Русский

Если X измерима и принимает значения в Icc[a,b] почти всюду, и μ конечна, то X интегрируема.

LaTeX

$$$\operatorname{AEStronglyMeasurable}(X, \mu) \wedge X(\omega) \in \mathrm{Icc}(a,b) \text{ a.e.} \Rightarrow \operatorname{Integrable}(X, \mu)$$$

Lean4

theorem of_mem_Icc_enorm [IsFiniteMeasure μ] {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) {X : α → ℝ≥0∞}
    (hX : AEMeasurable X μ) (h : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) : Integrable X μ :=
  ⟨hX.aestronglyMeasurable, .of_mem_Icc_of_ne_top ha hb h⟩

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