English
If s_i is a decreasing sequence of measurable sets with integrable f on their union, the integrals converge to the integral over the intersection.
Русский
Если s_i образуют убывающую последовательность измеримых множеств и f интегрируема на объединении, то интегралы сходятся к интегралу по пересечению.
LaTeX
$$$$ \lim_{i \to \infty} \int_{x \in s_i} f(x) \, d\mu = \int_{x \in \bigcap_{n} s_n} f(x) \, d\mu $$$$
Lean4
theorem tendsto_setIntegral_of_antitone {ι : Type*} [Preorder ι] [(atTop : Filter ι).IsCountablyGenerated]
{s : ι → Set X} (hsm : ∀ i, MeasurableSet (s i)) (h_anti : Antitone s) (hfi : ∃ i, IntegrableOn f (s i) μ) :
Tendsto (fun i ↦ ∫ x in s i, f x ∂μ) atTop (𝓝 (∫ x in ⋂ n, s n, f x ∂μ)) :=
by
refine .of_neBot_imp fun hne ↦ ?_
have := (atTop_neBot_iff.mp hne).2
rcases hfi with ⟨i₀, hi₀⟩
suffices
Tendsto (∫ x in s i₀, f x ∂μ - ∫ x in s i₀ \ s ·, f x ∂μ) atTop
(𝓝 (∫ x in s i₀, f x ∂μ - ∫ x in ⋃ i, s i₀ \ s i, f x ∂μ))
by
convert this.congr' <| (eventually_ge_atTop i₀).mono fun i hi ↦ ?_
· rw [← diff_iInter, integral_diff _ hi₀ (iInter_subset _ _), sub_sub_cancel]
exact .iInter_of_antitone h_anti hsm
· rw [integral_diff (hsm i) hi₀ (h_anti hi), sub_sub_cancel]
apply tendsto_const_nhds.sub
refine tendsto_setIntegral_of_monotone (by measurability) ?_ ?_
· exact fun i j h ↦ diff_subset_diff_right (h_anti h)
· rw [← diff_iInter]
exact hi₀.mono_set diff_subset
