lintegral_iInf — Mathlib

English

A variant of the tendsto result for antitone families with almost everywhere Tendsto to F.

Русский

Вариант теоремы с предельным переходом для антимонотонных семей функций и почти всюду сходимостью к F.

LaTeX

$$$(f : \\Nat \\to α \\to ENNReal) \\rightarrow (Tendsto...)$$

Lean4

/-- **Monotone convergence theorem** for nonincreasing sequences of functions. -/
theorem lintegral_iInf {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, Measurable (f n)) (h_anti : Antitone f)
    (h_fin : ∫⁻ a, f 0 a ∂μ ≠ ∞) : ∫⁻ a, ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ a, f n a ∂μ :=
  lintegral_iInf_ae h_meas (fun n => ae_of_all _ <| h_anti n.le_succ) h_fin

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