English
If s_n is monotone and the tail differences have finite sum, then μ(⋃ s_n) = sup_n μ(s_n).
Русский
Если s_n монотонна и сумма модуля разностей конечна, то μ(⋃ s_n) = sup_n μ(s_n).
LaTeX
$$$\\\\mu\\\\left\\\\(\\\\\\\\bigcup_{n} s_n\\\\right\\\\) = \\\\sup_{n} \\\\mu(s_n) \\\\text{ при } s_n \\subseteq s_{n+1} \\\\wedge \\\\sum_{k}^{\\\\infty} μ(s_{k+1}\\\\setminus s_k) < \\\\infty$$$
Lean4
/-- Let `μ` be an (outer) measure; let `s : ι → Set α` be a sequence of sets, `S = ⋃ n, s n`.
If `μ (S \ s n)` tends to zero along some nontrivial filter (usually `Filter.atTop` on `ι = ℕ`),
then `μ S = ⨆ n, μ (s n)`. -/
theorem measure_iUnion_of_tendsto_zero {ι} (μ : F) {s : ι → Set α} (l : Filter ι) [NeBot l]
(h0 : Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (𝓝 0)) : μ (⋃ n, s n) = ⨆ n, μ (s n) :=
by
refine le_antisymm ?_ <| iSup_le fun n ↦ measure_mono <| subset_iUnion _ _
set S := ⋃ n, s n
set M := ⨆ n, μ (s n)
have A : ∀ k, μ S ≤ M + μ (S \ s k) := fun k ↦
calc
μ S ≤ μ (S ∩ s k) + μ (S \ s k) := measure_le_inter_add_diff _ _ _
_ ≤ μ (s k) + μ (S \ s k) := by gcongr; apply inter_subset_right
_ ≤ M + μ (S \ s k) := by gcongr; exact le_iSup (μ ∘ s) k
have B : Tendsto (fun k ↦ M + μ (S \ s k)) l (𝓝 M) := by simpa using tendsto_const_nhds.add h0
exact ge_of_tendsto' B A
