English
If a content m is σ-additive on a set ring, then for a monotone sequence of sets, m of the union equals the limit of the partial sums; i.e., tends to m(⋃ f i).
Русский
Если m σ-аддитивно на кольце множеств, то для монотонной последовательности множеств предел сумм сходится к m(⋃).
LaTeX
$$Tendsto (n \mapsto m(f(n))) atTop (nhds (m(⋃ i, f(i))))$$
Lean4
/-- If an additive content is σ-additive on a set ring, then the content of a monotone sequence of
sets tends to the content of the union. -/
theorem tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum (hC : IsSetRing C)
(m_iUnion :
∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : (⋃ i, f i) ∈ C) (_hf_disj : Pairwise (Disjoint on f)),
m (⋃ i, f i) = ∑' i, m (f i))
⦃f : ℕ → Set α⦄ (hf_mono : Monotone f) (hf : ∀ i, f i ∈ C) (hf_Union : ⋃ i, f i ∈ C) :
Tendsto (fun n ↦ m (f n)) atTop (𝓝 (m (⋃ i, f i))) :=
by
rw [← iUnion_disjointed, m_iUnion _ (hC.disjointed_mem hf) (by rwa [iUnion_disjointed]) (disjoint_disjointed f)]
have h n : m (f n) = ∑ i ∈ range (n + 1), m (disjointed f i) :=
by
nth_rw 1 [← addContent_accumulate _ hC (disjoint_disjointed f) (hC.disjointed_mem hf), ← hf_mono.partialSups_eq, ←
partialSups_disjointed, partialSups_eq_biSup, Accumulate]
rfl
simp_rw [h]
refine (tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (disjointed f i))) 1).2 ?_
exact ENNReal.tendsto_nat_tsum _
