English
For nonnegative f, the integral equals the tail integral over t > 0 of the measure of {a : t < f(a)}.
Русский
Для неотрицательной f интеграл равен хвост-интегралу по t>0 меры множества {a: t < f(a)}.
LaTeX
$$$$ \\int f \\; d\\mu = \\int_{0}^{\\infty} \\mu\\{a : t < f(a)\\} \\, dt. $$$$
Lean4
/-- **Monotone convergence theorem**, version with `AEMeasurable` functions. -/
theorem lintegral_iSup' {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, AEMeasurable (f n) μ)
(h_mono : ∀ᵐ x ∂μ, Monotone fun n => f n x) : ∫⁻ a, ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ a, f n a ∂μ :=
by
simp_rw [← iSup_apply]
let p : α → (ℕ → ℝ≥0∞) → Prop := fun _ f' => Monotone f'
have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_mono
have h_ae_seq_mono : Monotone (aeSeq hf p) := by
intro n m hnm x
by_cases hx : x ∈ aeSeqSet hf p
· exact aeSeq.prop_of_mem_aeSeqSet hf hx hnm
· simp only [aeSeq, hx, if_false, le_rfl]
rw [lintegral_congr_ae (aeSeq.iSup hf hp).symm]
simp_rw [iSup_apply]
rw [lintegral_iSup (aeSeq.measurable hf p) h_ae_seq_mono]
congr with n
exact lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae hf hp n)
