English
Under the same assumptions, the equality of lintegrals holds for directed families indexed by a countable set.
Русский
Также сохраняется равенство интегралов для направленного семейства с счётной индексацией.
LaTeX
$$$$ \\text{(same as previous form with directed, measurable setup)} $$$$
Lean4
/-- Weaker version of the **monotone convergence theorem**. -/
theorem lintegral_iSup_ae {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable (f n)) (h_mono : ∀ n, ∀ᵐ a ∂μ, f n a ≤ f n.succ a) :
∫⁻ a, ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ a, f n a ∂μ := by
classical
let ⟨s, hs⟩ := exists_measurable_superset_of_null (ae_iff.1 (ae_all_iff.2 h_mono))
let g n a := if a ∈ s then 0 else f n a
have g_eq_f : ∀ᵐ a ∂μ, ∀ n, g n a = f n a := (measure_eq_zero_iff_ae_notMem.1 hs.2.2).mono fun a ha n => if_neg ha
calc
∫⁻ a, ⨆ n, f n a ∂μ = ∫⁻ a, ⨆ n, g n a ∂μ := lintegral_congr_ae <| g_eq_f.mono fun a ha => by simp only [ha]
_ = ⨆ n, ∫⁻ a, g n a ∂μ :=
(lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n)) (monotone_nat_of_le_succ fun n a => ?_))
_ = ⨆ n, ∫⁻ a, f n a ∂μ := by simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]
simp only [g]
split_ifs with h
· rfl
· have := Set.notMem_subset hs.1 h
simp only [not_forall, not_le, mem_setOf_eq, not_exists, not_lt] at this
exact this n
