English
If s_n is a monotone sequence of sets and the series of tail differences is not infinite, then μ(⋃ n s_n) = ⨆ n μ(s_n).
Русский
Если последовательность множеств s_n монотонна и сумма хвостовых различий не бесконечна, тогда μ(⋃ n s_n) = ⨆ n μ(s_n).
LaTeX
$$$\\\\mu\\\\left\\\\(\\\\\\\\bigcup_{n} s_n\\\\right\\\\) = \\\\Upsilon_n μ(s_n) \\\\text{ при } s_n \\subseteq s_{n+1} \\\\wedge \\\\sum_{k} μ(s_{k+1}\\\\setminus s_k) \\\\neq \\\\infty$$$
Lean4
/-- If `s : ℕ → Set α` is a monotone sequence of sets such that `∑' k, m (s (k + 1) \ s k) ≠ ∞`,
then `m (⋃ n, s n) = ⨆ n, m (s n)`. -/
theorem iUnion_nat_of_monotone_of_tsum_ne_top (m : OuterMeasure α) {s : ℕ → Set α} (h_mono : ∀ n, s n ⊆ s (n + 1))
(h0 : (∑' k, m (s (k + 1) \ s k)) ≠ ∞) : m (⋃ n, s n) = ⨆ n, m (s n) := by
classical
refine measure_iUnion_of_tendsto_zero m atTop ?_
refine tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_
refine
(m.mono ?_).trans
(measure_iUnion_le _)
-- Current goal: `(⋃ k, s k) \ s n ⊆ ⋃ k, s (k + n + 1) \ s (k + n)`
have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono
simp only [diff_subset_iff, iUnion_subset_iff]
intro i x hx
have : ∃ i, x ∈ s i := by exists i
rcases Nat.findX this with ⟨j, hj, hlt⟩
clear hx i
rcases le_or_gt j n with hjn | hnj
· exact Or.inl (h' hjn hj)
have : j - (n + 1) + n + 1 = j := by omega
refine Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)
· rwa [this]
· rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]
