English
Let μ be a finite measure on X and Es_i ⊆ X be pairwise disjoint, null-measurable. Then μ(⋃_{i≥n} Es_i) → 0 as n → ∞.
Русский
Пусть μ — конечная мера на X, Es_i ⊆ X попарно непересекаются и нуль-измеримы. Тогда μ(⋃_{i≥n} Es_i) → 0 при n → ∞.
LaTeX
$$$\lim_{n \to \infty} μ\Big(\bigcup_{i \ge n} E_i\Big) = 0$ (в смысле Tendsto).$$
Lean4
theorem tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint {X : Type*} [MeasurableSpace X] {μ : Measure X}
[IsFiniteMeasure μ] {Es : ℕ → Set X} (Es_mble : ∀ i, NullMeasurableSet (Es i) μ)
(Es_disj : Pairwise fun n m ↦ Disjoint (Es n) (Es m)) : Tendsto (μ ∘ fun n ↦ ⋃ i ≥ n, Es i) atTop (𝓝 0) :=
by
have decr : Antitone fun n ↦ ⋃ i ≥ n, Es i := fun n m hnm ↦
biUnion_mono (fun _ hi ↦ le_trans hnm hi) (fun _ _ ↦ subset_rfl)
have nothing : ⋂ n, ⋃ i ≥ n, Es i = ∅ :=
by
apply subset_antisymm _ (empty_subset _)
intro x hx
simp only [mem_iInter, mem_iUnion, exists_prop] at hx
obtain ⟨j, _, x_in_Es_j⟩ := hx 0
obtain ⟨k, k_gt_j, x_in_Es_k⟩ := hx (j + 1)
have oops := (Es_disj (Nat.ne_of_lt k_gt_j)).ne_of_mem x_in_Es_j x_in_Es_k
contradiction
have key := tendsto_measure_iInter_atTop (μ := μ) (fun n ↦ by measurability) decr ⟨0, measure_ne_top _ _⟩
simp only [nothing, measure_empty] at key
convert key
