of_mem_Icc_of_ne_top — Mathlib

English

If μ is finite and a,b ∈ ENNReal with a ≠ ∞ and b ≠ ∞, and X: α → ENNReal satisfies X(ω) ∈ Icc(a,b) almost everywhere, then HasFiniteIntegral X μ.

Русский

Пусть μ конечна, a,b ∈ ENNReal и a ≠ ∞, b ≠ ∞. Если X(ω) ∈ [a,b] почти везде, то HasFiniteIntegral X μ.

LaTeX

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

Lean4

theorem of_mem_Icc_of_ne_top [IsFiniteMeasure μ] {a b : ℝ≥0∞} (ha : a ≠ ⊤) (hb : b ≠ ⊤) {X : α → ℝ≥0∞}
    (h : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) : HasFiniteIntegral X μ :=
  by
  have : ‖max ‖a‖ₑ ‖b‖ₑ‖ₑ ≠ ⊤ := by simp [ha, hb]
  apply (hasFiniteIntegral_const_enorm this (μ := μ)).mono'_enorm
  filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω h₁ h₂ using by simp [h₂]

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