Documentation

Mathlib.MeasureTheory.Measure.AddContent

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 #

Main statements #

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

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

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 Cself.toFun (⋃₀ I) = uI, self.toFun u
Instances For
    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) = uI, self.toFun u
    Equations
    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) = uI, 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 : tI, t s) (h_dis : (I).PairwiseDisjoint id) :
    m s = iI, m i + ihC.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 : sI, s t) :
    uI, 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 : nS, s n C) :
    m (iS, s i) iS, 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)