English
If (s_n) is a decreasing sequence of measurable sets and f is integrable on s_0, then ∫ f on s_n converges to ∫ f on ⋂ s_n as n→∞.
Русский
Если (s_n) — убывающая последовательность измеримых множеств и f интегрируема на s_0, то интеграл по s_n сходится к интегралу по ⋂ s_n.
LaTeX
$$$\\lim_{n\\to\\infty} \\int_{s_n} f \\,dμ = \\int_{\\bigcap_n s_n} f \\,dμ$$$
Lean4
theorem _root_.Antitone.tendsto_setIntegral (hsm : ∀ i, MeasurableSet (s i)) (h_anti : Antitone s)
(hfi : IntegrableOn f (s 0) μ) : Tendsto (fun i => ∫ a in s i, f a ∂μ) atTop (𝓝 (∫ a in ⋂ n, s n, f a ∂μ)) :=
by
let bound : α → ℝ := indicator (s 0) fun a => ‖f a‖
have h_int_eq : (fun i => ∫ a in s i, f a ∂μ) = fun i => ∫ a, (s i).indicator f a ∂μ :=
funext fun i => (integral_indicator (hsm i)).symm
rw [h_int_eq]
rw [← integral_indicator (MeasurableSet.iInter hsm)]
refine tendsto_integral_of_dominated_convergence bound ?_ ?_ ?_ ?_
· intro n
rw [aestronglyMeasurable_indicator_iff (hsm n)]
exact (IntegrableOn.mono_set hfi (h_anti (zero_le n))).1
· rw [integrable_indicator_iff (hsm 0)]
exact hfi.norm
· simp_rw [norm_indicator_eq_indicator_norm]
refine fun n => Eventually.of_forall fun x => ?_
exact indicator_le_indicator_of_subset (h_anti (zero_le n)) (fun a => norm_nonneg _) _
· filter_upwards [] with a using le_trans (h_anti.tendsto_indicator _ _ _) (pure_le_nhds _)
