σ-additivity of inner regular contents

An additive content on a ring of sets which is inner regular with respect to a compact system contained in the ring is σ-additive.

Main statements

• tendsto_zero_of_innerRegular_addContent: such a content is continuous at ∅.
• addContent_iUnion_eq_sum_of_innerRegular: such a content is σ-additive, if it takes finite values.

theorem MeasureTheory.tendsto_zero_of_innerRegular_addContent {α : Type u_1} {C R : Set (Set α)} {s : ℕ → Set α} (hR : IsSetRing R) (m : AddContent ENNReal R) (hs : ∀ (n : ℕ), s n ∈ R) (hs_anti : Antitone s) (hs_iInter : ⋂ (n : ℕ), s n = ∅) (hC : IsCompactSystem C) (hCR : C ⊆ R) (h_reg : ∀ A ∈ R, ∀ (ε : ENNReal), 0 < ε → ∃ K ∈ C, K ⊆ A ∧ m (A \ K) ≤ ε) : Filter.Tendsto (fun (n : ℕ) => m (s n)) Filter.atTop (nhds 0)

Let m be an additive content on a ring of sets R, inner regular with respect to a compact system C ⊆ R: every set of R can be approximated from inside by sets of C. Then m is continuous at ∅: if s is a decreasing sequence of sets of R with empty intersection, then m (s n) tends to 0.

theorem MeasureTheory.addContent_iUnion_eq_sum_of_innerRegular {α : Type u_1} {C R : Set (Set α)} (hR : IsSetRing R) (m : AddContent ENNReal R) (hm_ne_top : ∀ s ∈ R, m s ≠ ⊤) (hC : IsCompactSystem C) (hCR : C ⊆ R) (h_reg : ∀ A ∈ R, ∀ (ε : ENNReal), 0 < ε → ∃ K ∈ C, K ⊆ A ∧ m (A \ K) ≤ ε) ⦃f : ℕ → Set α⦄ (hf : ∀ (i : ℕ), f i ∈ R) (hUf : ⋃ (i : ℕ), f i ∈ R) (h_disj : Pairwise (Function.onFun Disjoint f)) : m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), m (f i)

An additive content with finite values on a ring of sets R, which is inner regular with respect to a compact system C ⊆ R, is σ-additive.