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 G C: additive contents over the set of sets C taking values in the additive monoid G.
• MeasureTheory.AddContent.IsSigmaSubadditive: an AddContent with values in ℝ≥0∞ is σ-subadditive if m (⋃ i, f i) ≤ ∑' i, m (f i) for any sequence of sets f in C such that ⋃ i, f i ∈ C.

Main statements

Let m be an AddContent C with values in ℝ≥0∞. 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_sUnion_le_sum: an AddContent C on a SetSemiring C is sub-additive.
• MeasureTheory.addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le: if an AddContent is σ-subadditive on a semi-ring of sets, then it is σ-additive.
• 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

• MeasureTheory.addContent_union_le: for s, t ∈ C, m (s ∪ t) ≤ m s + m t
• MeasureTheory.addContent_le_diff: for s, t ∈ C, m s - m t ≤ m (s \ t)
• IsSetRing.addContent_of_union: a function on a ring of sets which is additive on pairs of disjoint sets defines an additive content
• addContent_iUnion_eq_sum_of_tendsto_zero: if an additive content is continuous at ∅, then its value on a countable disjoint union is the sum of the values
• MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum: if an AddContent is σ-additive on a set ring, then it is σ-subadditive.

We define a specific example of AddContent, called AddContent.onIoc, on the semiring of sets made of open-closed intervals, mapping (a, b] to f b - f a.

structure MeasureTheory.AddContent {α : Type u_1} (G : Type u_2) [AddCommMonoid G] (C : Set (Set α)) : Type (max u_1 u_2)

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 α → G

  The value of the content on a set.

• empty' : self.toFun ∅ = 0
• sUnion' (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 α)} {G : Type u_2} [AddCommMonoid G] : Inhabited (AddContent G C)

Equations

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

instance MeasureTheory.instFunLikeAddContentSet {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] : FunLike (AddContent G C) (Set α) G

Equations

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

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

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

@[simp]

theorem MeasureTheory.addContent_empty {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} : m ∅ = 0

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

theorem MeasureTheory.addContent_biUnion {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} {ι : Type u_3} {a : Finset ι} {f : ι → Set α} (hf : ∀ i ∈ a, f i ∈ C) (h_dis : (↑a).PairwiseDisjoint f) (h_mem : ⋃ i ∈ a, f i ∈ C) : m (⋃ i ∈ a, f i) = ∑ i ∈ a, m (f i)

theorem MeasureTheory.addContent_iUnion {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} {ι : Type u_3} [Fintype ι] {f : ι → Set α} (hf : ∀ (i : ι), f i ∈ C) (h_dis : Pairwise (Function.onFun Disjoint f)) (h_mem : ⋃ (i : ι), f i ∈ C) : m (⋃ (i : ι), f i) = ∑ i : ι, m (f i)

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

def MeasureTheory.AddContent.IsSigmaSubadditive {α : Type u_1} {C : Set (Set α)} (m : AddContent ENNReal C) : Prop

An additive content with values in ℝ≥0∞ is said to be sigma-sub-additive if for any sequence of sets f in C such that ⋃ i, f i ∈ C, we have m (⋃ i, f i) ≤ ∑' i, m (f i).

Equations

• m.IsSigmaSubadditive = ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → m (⋃ (i : ℕ), f i) ≤ ∑' (i : ℕ), m (f i)

theorem MeasureTheory.addContent_eq_add_disjointOfDiffUnion_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} (hC : 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.disjointOfDiffUnion hs hI, m i

theorem MeasureTheory.eq_add_disjointOfDiff_of_subset {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) : m t = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

For an m : addContent C on a SetSemiring C and s t : Set α with s ⊆ t, we can write m t = m s + ∑ i in hC.disjointOfDiff ht hs, m i.

theorem MeasureTheory.sum_addContent_eq_of_sUnion_eq {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} (hC : IsSetSemiring C) (J J' : Finset (Set α)) (hJ : ↑J ⊆ C) (hJdisj : (↑J).PairwiseDisjoint id) (hJ' : ↑J' ⊆ C) (hJ'disj : (↑J').PairwiseDisjoint id) (h : ⋃₀ ↑J = ⋃₀ ↑J') : ∑ s ∈ J, m s = ∑ t ∈ J', m t

If a set can be written in two different ways as a disjoint union of elements of a semi-ring of sets C, then the sums of the values of m : addContent C along the two decompositions give the same result. In other words, m can be canonically extended to finite unions of elements of C.

noncomputable def MeasureTheory.AddContent.supClosure {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] (m : AddContent G C) (hC : IsSetSemiring C) : AddContent G (_root_.supClosure C)

Extend a content over C to the finite unions of elements of C by additivity.

Equations

• m.supClosure hC = { toFun := MeasureTheory.AddContent.supClosureFun✝ m, empty' := ⋯, sUnion' := ⋯ }

theorem MeasureTheory.AddContent.supClosure_apply {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] (hC : IsSetSemiring C) (m : AddContent G C) {s : Set α} {J : Finset (Set α)} (hJ : ↑J ⊆ C) (h'J : (↑J).PairwiseDisjoint id) (hs : s = ⋃₀ ↑J) : (m.supClosure hC) s = ∑ s ∈ J, m s

theorem MeasureTheory.AddContent.supClosure_apply_finpartition {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] (hC : IsSetSemiring C) (m : AddContent G C) {s : Set α} {J : Finpartition s} (hJ : ↑J.parts ⊆ C) : (m.supClosure hC) s = ∑ s ∈ J.parts, m s

theorem MeasureTheory.AddContent.supClosure_apply_of_mem {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] (hC : IsSetSemiring C) (m : AddContent G C) {s : Set α} (hs : s ∈ C) : (m.supClosure hC) s = m s

theorem MeasureTheory.sum_addContent_le_of_subset {α : Type u_1} {C : Set (Set α)} {t : Set α} {I : Finset (Set α)} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} [PartialOrder G] [CanonicallyOrderedAdd G] (hC : 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

For an m : addContent C on a SetSemiring C, if I is a Finset of pairwise disjoint sets in C and ⋃₀ I ⊆ t for t ∈ C, then ∑ s ∈ I, m s ≤ m t.

theorem MeasureTheory.addContent_mono {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} [PartialOrder G] [CanonicallyOrderedAdd G] (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) : m s ≤ m t

An addContent C on a SetSemiring C is monotone.

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

An addContent C on a SetSemiring C is sub-additive.

theorem MeasureTheory.addContent_le_sum_of_subset_sUnion {α : Type u_1} {C : Set (Set α)} {t : Set α} {G : Type u_2} [AddCommMonoid G] [PartialOrder G] [CanonicallyOrderedAdd G] {m : AddContent G C} (hC : 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 : AddContent ENNReal C} (hC : IsSetSemiring C) (m_subadd : ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → Pairwise (Function.onFun Disjoint 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 (Function.onFun Disjoint 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_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive {α : Type u_1} {C : Set (Set α)} {m : AddContent ENNReal C} (hC : IsSetSemiring C) (m_subadd : m.IsSigmaSubadditive) (f : ℕ → Set α) (hf : ∀ (i : ℕ), f i ∈ C) (hf_Union : ⋃ (i : ℕ), f i ∈ C) (hf_disj : Pairwise (Function.onFun Disjoint f)) : m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), m (f i)

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

noncomputable def MeasureTheory.AddContent.onIocAux {α : Type u_1} [LinearOrder α] {G : Type u_3} [AddCommGroup G] (f : α → G) (s : Set α) : G

The function associating to an interval Ioc u v the difference f v - f u. Use instead AddContent.ofIoc which upgrades this function to an additive content.

Equations

• MeasureTheory.AddContent.onIocAux f s = if h : ∃ (p : α × α), p.1 ≤ p.2 ∧ s = Set.Ioc p.1 p.2 then f h.choose.2 - f h.choose.1 else 0

theorem MeasureTheory.AddContent.onIocAux_apply {α : Type u_1} [LinearOrder α] {G : Type u_3} [AddCommGroup G] {f : α → G} {u v : α} (h : u ≤ v) : onIocAux f (Set.Ioc u v) = f v - f u

theorem MeasureTheory.AddContent.onIocAux_empty {α : Type u_1} [LinearOrder α] {G : Type u_3} [AddCommGroup G] (f : α → G) : onIocAux f ∅ = 0

noncomputable def MeasureTheory.AddContent.onIoc {α : Type u_1} [LinearOrder α] {G : Type u_3} [AddCommGroup G] (f : α → G) : AddContent G {s : Set α | ∃ (u : α) (v : α), u ≤ v ∧ s = Set.Ioc u v}

The additive content on the set of open-closed intervals, associating to an interval Ioc u v the difference f v - f u.

Equations

• MeasureTheory.AddContent.onIoc f = { toFun := MeasureTheory.AddContent.onIocAux f, empty' := ⋯, sUnion' := ⋯ }

theorem MeasureTheory.AddContent.onIoc_apply {α : Type u_1} [LinearOrder α] {G : Type u_3} [AddCommGroup G] {f : α → G} {u v : α} (h : u ≤ v) : (onIoc f) (Set.Ioc u v) = f v - f u

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

An additive content obtained from another one on the same semiring of sets by setting the value of each set not in the semiring at ∞.

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 : IsSetSemiring C) (m : AddContent ENNReal C) : ⇑(AddContent.extend hC m) = extend fun (x : Set α) (x_1 : x ∈ C) => m x

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

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

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

theorem MeasureTheory.addContent_biUnion_eq {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} {ι : Type u_3} (hC : IsSetRing C) {s : ι → Set α} {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C) (hS : (↑S).PairwiseDisjoint s) : m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)

theorem MeasureTheory.addContent_accumulate {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] (m : AddContent G C) (hC : IsSetRing C) {s : ℕ → Set α} (hs_disj : Pairwise (Function.onFun Disjoint s)) (hsC : ∀ (i : ℕ), s i ∈ C) (n : ℕ) : m (Set.accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)

def MeasureTheory.IsSetRing.addContent_of_union {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [AddCommMonoid G] (m : Set α → G) (hC : IsSetRing C) (m_empty : m ∅ = 0) (m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t) : AddContent G C

A function which is additive on disjoint elements in a ring of sets C defines an additive content on C.

Equations

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

theorem MeasureTheory.addContent_union_le {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} [PartialOrder G] [CanonicallyOrderedAdd G] (hC : 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 α)} {G : Type u_2} [AddCommMonoid G] {m : AddContent G C} [PartialOrder G] [CanonicallyOrderedAdd G] {ι : Type u_3} (hC : 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 t : Set α} (m : AddContent ENNReal C) (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : m s - m t ≤ m (s \ t)

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

theorem MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero {α : Type u_1} {C : Set (Set α)} (hC : IsSetRing C) (m : AddContent ENNReal C) (hm_ne_top : ∀ s ∈ C, m s ≠ ⊤) (hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ (n : ℕ), s n = ∅ → Filter.Tendsto (fun (n : ℕ) => m (s n)) Filter.atTop (nhds 0)) ⦃f : ℕ → Set α⦄ (hf : ∀ (i : ℕ), f i ∈ C) (hUf : ⋃ (i : ℕ), f i ∈ C) (h_disj : Pairwise (Function.onFun Disjoint f)) : m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), m (f i)

In a ring of sets, continuity of an additive content at ∅ implies σ-additivity. This is not true in general in semirings, or without the hypothesis that m is finite. See the examples 7 and 8 in Halmos' book Measure Theory (1974), page 40.

theorem MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum {α : Type u_1} {C : Set (Set α)} {m : AddContent ENNReal C} (hC : IsSetRing C) (m_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → Pairwise (Function.onFun Disjoint 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.isSigmaSubadditive_of_addContent_iUnion_eq_tsum {α : Type u_1} {C : Set (Set α)} {m : AddContent ENNReal C} (hC : IsSetRing C) (m_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ (i : ℕ), f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), m (f i)) : m.IsSigmaSubadditive

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