of_mem_Icc — Mathlib

English

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

Русский

Если μ конечна и X: α → ℝ удовлетворяет X(ω)∈[a,b] почти всюду, тогда HasFiniteIntegral X μ.

LaTeX

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

Lean4

theorem of_mem_Icc [IsFiniteMeasure μ] (a b : ℝ) {X : α → ℝ} (h : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) : HasFiniteIntegral X μ :=
  by
  apply (hasFiniteIntegral_const (max ‖a‖ ‖b‖)).mono'
  filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω using abs_le_max_abs_abs

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