σ-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))
:
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.