noncomputable def MeasureTheory.extendContent {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : (s : Set α) → s ∈ C → ENNReal) (m_empty : m ∅ ⋯ = 0) (m_add : ∀ (I : Finset (Set α)) (h_ss : ↑I ⊆ C), (↑I).PairwiseDisjoint id → ∀ (h_mem : ⋃₀ ↑I ∈ C), m (⋃₀ ↑I) h_mem = ∑ u : { x : Set α // x ∈ I }, m ↑u ⋯) : MeasureTheory.AddContent C

Build an AddContent from an additive function defined on a semiring.

Equations

• MeasureTheory.extendContent hC m m_empty m_add = { toFun := MeasureTheory.extend m, empty' := ⋯, sUnion' := ⋯ }

theorem MeasureTheory.extendContent_eq_extend {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : (s : Set α) → s ∈ C → ENNReal) (m_empty : m ∅ ⋯ = 0) (m_add : ∀ (I : Finset (Set α)) (h_ss : ↑I ⊆ C), (↑I).PairwiseDisjoint id → ∀ (h_mem : ⋃₀ ↑I ∈ C), m (⋃₀ ↑I) h_mem = ∑ u : { x : Set α // x ∈ I }, m ↑u ⋯) : ⇑(MeasureTheory.extendContent hC m m_empty m_add) = MeasureTheory.extend m

theorem MeasureTheory.extendContent_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C) (m : (s : Set α) → s ∈ C → ENNReal) (m_empty : m ∅ ⋯ = 0) (m_add : ∀ (I : Finset (Set α)) (h_ss : ↑I ⊆ C), (↑I).PairwiseDisjoint id → ∀ (h_mem : ⋃₀ ↑I ∈ C), m (⋃₀ ↑I) h_mem = ∑ u : { x : Set α // x ∈ I }, m ↑u ⋯) (hs : s ∈ C) : (MeasureTheory.extendContent hC m m_empty m_add) s = m s hs

theorem MeasureTheory.extendContent_eq_top {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C) (m : (s : Set α) → s ∈ C → ENNReal) (m_empty : m ∅ ⋯ = 0) (m_add : ∀ (I : Finset (Set α)) (h_ss : ↑I ⊆ C), (↑I).PairwiseDisjoint id → ∀ (h_mem : ⋃₀ ↑I ∈ C), m (⋃₀ ↑I) h_mem = ∑ u : { x : Set α // x ∈ I }, m ↑u ⋯) (hs : s ∉ C) : (MeasureTheory.extendContent hC m m_empty m_add) s = ⊤

noncomputable def MeasureTheory.AddContent.extend {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) : MeasureTheory.AddContent C

Equations

• MeasureTheory.AddContent.extend hC m = { toFun := MeasureTheory.extend fun (x : Set α) (x_1 : x ∈ C) => m x, empty' := ⋯, sUnion' := ⋯ }

theorem MeasureTheory.AddContent.extend_eq_extend {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) : ⇑(MeasureTheory.AddContent.extend hC m) = MeasureTheory.extend fun (x : Set α) (x_1 : x ∈ C) => m x

theorem MeasureTheory.AddContent.extend_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) (hs : s ∈ C) : (MeasureTheory.AddContent.extend hC m) s = m s

theorem MeasureTheory.AddContent.extend_eq_top {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent C) (hs : s ∉ C) : (MeasureTheory.AddContent.extend hC m) s = ⊤

theorem MeasureTheory.addContent_sUnion_le_sum {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (h_ss : ↑J ⊆ C) (h_mem : ⋃₀ ↑J ∈ C) : m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

theorem MeasureTheory.addContent_le_sum_of_subset_sUnion {α : Type u_1} {C : Set (Set α)} {t : Set α} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (h_ss : ↑J ⊆ C) (ht : t ∈ C) (htJ : t ⊆ ⋃₀ ↑J) : m t ≤ ∑ u ∈ J, m u

theorem MeasureTheory.addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetSemiring C) (m_subadd : ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)) (f : ℕ → Set α) (hf : ∀ (i : ℕ), f i ∈ C) (hf_Union : ⋃ (i : ℕ), f i ∈ C) (hf_disj : Pairwise (Disjoint on f)) : m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), m (f i)

If an AddContent is σ-subadditive on a semi-ring of sets, then it is σ-additive.

theorem MeasureTheory.addContent_diff_of_ne_top {α : Type u_1} {C : Set (Set α)} (m : MeasureTheory.AddContent C) (hC : MeasureTheory.IsSetRing C) (hm_ne_top : ∀ s ∈ C, m s ≠ ⊤) {s : Set α} {t : Set α} (hs : s ∈ C) (ht : t ∈ C) (hts : t ⊆ s) : m (s \ t) = m s - m t

theorem MeasureTheory.addContent_accumulate {α : Type u_1} {C : Set (Set α)} (m : MeasureTheory.AddContent C) (hC : MeasureTheory.IsSetRing C) {s : ℕ → Set α} (hs_disj : Pairwise (Disjoint on s)) (hsC : ∀ (i : ℕ), s i ∈ C) (n : ℕ) : m (Set.Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)

theorem MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetRing C) (m_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → 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) : Filter.Tendsto (fun (n : ℕ) => m (f n)) Filter.atTop (nhds (m (⋃ (i : ℕ), f i)))

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 MeasureTheory.addContent_iUnion_le_of_addContent_iUnion_eq_tsum {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetRing C) (m_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), m (f i)) (f : ℕ → Set α) (hf : ∀ (i : ℕ), f i ∈ C) (hf_Union : ⋃ (i : ℕ), f i ∈ C) : m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)

If an additive content is σ-additive on a set ring, then it is σ-subadditive.