English
In a ring of sets, disjoint unions over any index family yield additivity of the content across the union.
Русский
В кольце множеств суммарная аддитивность содержимого распространяется на обобщённые объединения по индексам.
LaTeX
$$m(\bigcup_{i} s(i)) = \sum_{i} m(s(i))$$
Lean4
/-- In a ring of sets, continuity of an additive content at `∅` implies σ-additivity.
This is not true in general in semirings, or without the hypothesis that `m` is finite. See the
examples 7 and 8 in Halmos' book Measure Theory (1974), page 40. -/
theorem addContent_iUnion_eq_sum_of_tendsto_zero (hC : IsSetRing C) (m : AddContent C) (hm_ne_top : ∀ s ∈ C, m s ≠ ∞)
(hm_tendsto :
∀ ⦃s : ℕ → Set α⦄ (_ : ∀ n, s n ∈ C), Antitone s → (⋂ n, s n) = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0))
⦃f : ℕ → Set α⦄ (hf : ∀ i, f i ∈ C) (hUf : (⋃ i, f i) ∈ C) (h_disj : Pairwise (Disjoint on f)) :
m (⋃ i, f i) = ∑' i, m (f i) := by
-- We use the continuity of `m` at `∅` on the sequence `n ↦ (⋃ i, f i) \ (set.accumulate f n)`
let s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ Set.Accumulate f n
have hCs n : s n ∈ C := hC.diff_mem hUf (hC.accumulate_mem hf n)
have h_tendsto : Tendsto (fun n ↦ m (s n)) atTop (𝓝 0) :=
by
refine hm_tendsto hCs ?_ ?_
· intro i j hij x hxj
rw [Set.mem_diff] at hxj ⊢
exact ⟨hxj.1, fun hxi ↦ hxj.2 (Set.monotone_accumulate hij hxi)⟩
· simp_rw [s, Set.diff_eq]
rw [Set.iInter_inter_distrib, Set.iInter_const, ← Set.compl_iUnion, Set.iUnion_accumulate]
exact Set.inter_compl_self _
have hmsn n : m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i) := by
rw [addContent_diff_of_ne_top m hC hm_ne_top hUf (hC.accumulate_mem hf n) (Set.accumulate_subset_iUnion _),
addContent_accumulate m hC h_disj hf n]
simp_rw [hmsn] at h_tendsto
refine tendsto_nhds_unique ?_ (ENNReal.tendsto_nat_tsum fun i ↦ m (f i))
refine (Filter.tendsto_add_atTop_iff_nat 1).mp ?_
rwa [ENNReal.tendsto_const_sub_nhds_zero_iff (hm_ne_top _ hUf) (fun n ↦ ?_)] at h_tendsto
rw [← addContent_accumulate m hC h_disj hf]
exact addContent_mono hC.isSetSemiring (hC.accumulate_mem hf n) hUf (Set.accumulate_subset_iUnion _)
