Additive Contents

An additive content m on a set of sets C is a set function with value 0 at the empty set which is finitely additive on C. That means that for any finset I of pairwise disjoint sets in C such that ⋃₀ I ∈ C, m (⋃₀ I) = ∑ s ∈ I, m s.

Mathlib also has a definition of contents over compact sets: see MeasureTheory.Content. A Content is in particular an AddContent on the set of compact sets.

Main definitions

• MeasureTheory.AddContent C: additive contents over the set of sets C.

Main statements

Let m be an AddContent C. If C is a set semi-ring (IsSetSemiring C) we have the properties

• MeasureTheory.sum_addContent_le_of_subset: if I is a finset of pairwise disjoint sets in C and ⋃₀ I ⊆ t for t ∈ C, then ∑ s ∈ I, m s ≤ m t.
• MeasureTheory.addContent_mono: if s ⊆ t for two sets in C, then m s ≤ m t.
• MeasureTheory.addContent_union': if s, t ∈ C are disjoint and s ∪ t ∈ C, then m (s ∪ t) = m s + m t. If C is a set ring (IsSetRing), then addContent_union gives the same conclusion without the hypothesis s ∪ t ∈ C (since it is a consequence of IsSetRing C).

If C is a set ring (MeasureTheory.IsSetRing C), we have, for s, t ∈ C,

• MeasureTheory.addContent_union_le: m (s ∪ t) ≤ m s + m t
• MeasureTheory.addContent_le_diff: m s - m t ≤ m (s \ t)

structure MeasureTheory.AddContent {α : Type u_1} (C : Set (Set α)) : Type u_1

An additive content is a set function with value 0 at the empty set which is finitely additive on a given set of sets.

• toFun : Set α → ENNReal

  The value of the content on a set.

• empty' : self.toFun ∅ = 0
• sUnion' : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → self.toFun (⋃₀ ↑I) = ∑ u ∈ I, self.toFun u

theorem MeasureTheory.AddContent.empty' {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.AddContent C) : self.toFun ∅ = 0

theorem MeasureTheory.AddContent.sUnion' {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.AddContent C) (I : Finset (Set α)) (_h_ss : ↑I ⊆ C) (_h_dis : (↑I).PairwiseDisjoint id) (_h_mem : ⋃₀ ↑I ∈ C) : self.toFun (⋃₀ ↑I) = ∑ u ∈ I, self.toFun u

instance MeasureTheory.instInhabitedAddContent {α : Type u_1} {C : Set (Set α)} : Inhabited (MeasureTheory.AddContent C)

Equations

• MeasureTheory.instInhabitedAddContent = { default := { toFun := fun (x : Set α) => 0, empty' := MeasureTheory.instInhabitedAddContent.proof_1, sUnion' := ⋯ } }

instance MeasureTheory.instDFunLikeAddContentSetENNReal {α : Type u_1} {C : Set (Set α)} : DFunLike (MeasureTheory.AddContent C) (Set α) fun (x : Set α) => ENNReal

Equations

• MeasureTheory.instDFunLikeAddContentSetENNReal = { coe := fun (m : MeasureTheory.AddContent C) (s : Set α) => m.toFun s, coe_injective' := ⋯ }

theorem MeasureTheory.AddContent.ext {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent C} {m' : MeasureTheory.AddContent C} (h : ∀ (s : Set α), m s = m' s) : m = m'

theorem MeasureTheory.AddContent.ext_iff {α : Type u_1} {C : Set (Set α)} (m : MeasureTheory.AddContent C) (m' : MeasureTheory.AddContent C) : m = m' ↔ ∀ (s : Set α), m s = m' s

@[simp]

theorem MeasureTheory.addContent_empty {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent C} : m ∅ = 0

theorem MeasureTheory.addContent_sUnion {α : Type u_1} {C : Set (Set α)} {I : Finset (Set α)} {m : MeasureTheory.AddContent C} (h_ss : ↑I ⊆ C) (h_dis : (↑I).PairwiseDisjoint id) (h_mem : ⋃₀ ↑I ∈ C) : m (⋃₀ ↑I) = ∑ u ∈ I, m u

theorem MeasureTheory.addContent_union' {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} {m : MeasureTheory.AddContent C} (hs : s ∈ C) (ht : t ∈ C) (hst : s ∪ t ∈ C) (h_dis : Disjoint s t) : m (s ∪ t) = m s + m t

theorem MeasureTheory.addContent_eq_add_diffFinset₀_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (hI_ss : ∀ t ∈ I, t ⊆ s) (h_dis : (↑I).PairwiseDisjoint id) : m s = ∑ i ∈ I, m i + ∑ i ∈ hC.diffFinset₀ hs hI, m i

theorem MeasureTheory.sum_addContent_le_of_subset {α : Type u_1} {C : Set (Set α)} {t : Set α} {I : Finset (Set α)} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetSemiring C) (h_ss : ↑I ⊆ C) (h_dis : (↑I).PairwiseDisjoint id) (ht : t ∈ C) (hJt : ∀ s ∈ I, s ⊆ t) : ∑ u ∈ I, m u ≤ m t

theorem MeasureTheory.addContent_mono {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) : m s ≤ m t

theorem MeasureTheory.addContent_union {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) (h_dis : Disjoint s t) : m (s ∪ t) = m s + m t

theorem MeasureTheory.addContent_union_le {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : m (s ∪ t) ≤ m s + m t

theorem MeasureTheory.addContent_biUnion_le {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent C} {ι : Type u_2} (hC : MeasureTheory.IsSetRing C) {s : ι → Set α} {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C) : m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)

theorem MeasureTheory.le_addContent_diff {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (m : MeasureTheory.AddContent C) (hC : MeasureTheory.IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : m s - m t ≤ m (s \ t)