Documentation

Mathlib.MeasureTheory.SetSemiring

Semirings and rings of sets #

A semi-ring of sets C (in the sense of measure theory) is a family of sets containing , stable by intersection and such that for all s, t ∈ C, t \ s is equal to a disjoint union of finitely many sets in C. Note that a semi-ring of sets may not contain unions.

An important example of a semi-ring of sets is intervals in . The intersection of two intervals is an interval (possibly empty). The union of two intervals may not be an interval. The set difference of two intervals may not be an interval, but it will be a disjoint union of two intervals.

A ring of sets is a set of sets containing , stable by union, set difference and intersection.

Main definitions #

Main statements #

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

A semi-ring of sets C is a family of sets containing , stable by intersection and such that for all s, t ∈ C, s \ t is equal to a disjoint union of finitely many sets in C.

  • empty_mem : C
  • inter_mem : sC, tC, s t C
  • diff_eq_sUnion' : sC, tC, ∃ (I : Finset (Set α)), I C (↑I).PairwiseDisjoint id s \ t = ⋃₀ I
Instances For
    theorem MeasureTheory.IsSetSemiring.inter_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetSemiring C) (s : Set α) :
    s CtC, s t C
    theorem MeasureTheory.IsSetSemiring.diff_eq_sUnion' {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetSemiring C) (s : Set α) :
    s CtC, ∃ (I : Finset (Set α)), I C (↑I).PairwiseDisjoint id s \ t = ⋃₀ I
    noncomputable def MeasureTheory.IsSetSemiring.diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) :
    Finset (Set α)

    In a semi-ring of sets C, for all sets s, t ∈ C, s \ t is equal to a disjoint union of finitely many sets in C. The finite set of sets in the union is not unique, but this definition gives an arbitrary Finset (Set α) that satisfies the equality.

    We remove the empty set to ensure that t ∉ hC.diffFinset hs ht even if t = ∅.

    Equations
    • hC.diffFinset hs ht = .choose \ {}
    Instances For
      theorem MeasureTheory.IsSetSemiring.empty_not_mem_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) :
      hC.diffFinset hs ht
      theorem MeasureTheory.IsSetSemiring.diffFinset_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) :
      (hC.diffFinset hs ht) C
      theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) :
      (↑(hC.diffFinset hs ht)).PairwiseDisjoint id
      theorem MeasureTheory.IsSetSemiring.sUnion_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) :
      ⋃₀ (hC.diffFinset hs ht) = s \ t
      theorem MeasureTheory.IsSetSemiring.not_mem_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) :
      thC.diffFinset hs ht
      theorem MeasureTheory.IsSetSemiring.sUnion_insert_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) (hst : t s) :
      ⋃₀ insert t (hC.diffFinset hs ht) = s
      theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) :
      Disjoint t (⋃₀ (hC.diffFinset hs ht))
      theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (ht : t C) :
      (insert t (hC.diffFinset hs ht)).PairwiseDisjoint id
      theorem MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
      ∃ (J : Finset (Set α)), J C (↑J).PairwiseDisjoint id s \ ⋃₀ I = ⋃₀ J

      In a semiring of sets C, for all set s ∈ C and finite set of sets I ⊆ C, there is a finite set of sets in C whose union is s \ ⋃₀ I. See IsSetSemiring.diffFinset₀ for a definition that gives such a set.

      noncomputable def MeasureTheory.IsSetSemiring.diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
      Finset (Set α)

      In a semiring of sets C, for all set s ∈ C and finite set of sets I ⊆ C, diffFinset₀ is a finite set of sets in C such that s \ ⋃₀ I = ⋃₀ (hC.diffFinset₀ hs I hI). diffFinset is a special case of diffFinset₀ where I is a singleton.

      Equations
      • hC.diffFinset₀ hs hI = .choose \ {}
      Instances For
        theorem MeasureTheory.IsSetSemiring.empty_not_mem_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
        hC.diffFinset₀ hs hI
        theorem MeasureTheory.IsSetSemiring.diffFinset₀_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
        (hC.diffFinset₀ hs hI) C
        theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
        (↑(hC.diffFinset₀ hs hI)).PairwiseDisjoint id
        theorem MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
        s \ ⋃₀ I = ⋃₀ (hC.diffFinset₀ hs hI)
        theorem MeasureTheory.IsSetSemiring.sUnion_diffFinset₀_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
        ⋃₀ (hC.diffFinset₀ hs hI) s
        theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
        Disjoint (⋃₀ I) (⋃₀ (hC.diffFinset₀ hs hI))
        theorem MeasureTheory.IsSetSemiring.disjoint_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) :
        Disjoint I (hC.diffFinset₀ hs hI)
        theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) (h_dis : (↑I).PairwiseDisjoint id) :
        (I (hC.diffFinset₀ hs hI)).PairwiseDisjoint id
        theorem MeasureTheory.IsSetSemiring.sUnion_union_sUnion_diffFinset₀_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) (hI_ss : tI, t s) :
        ⋃₀ I ⋃₀ (hC.diffFinset₀ hs hI) = s
        theorem MeasureTheory.IsSetSemiring.sUnion_union_diffFinset₀_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s C) (hI : I C) (hI_ss : tI, t s) [DecidableEq (Set α)] :
        ⋃₀ (I hC.diffFinset₀ hs hI) = s
        structure MeasureTheory.IsSetRing {α : Type u_1} (C : Set (Set α)) :

        A ring of sets C is a family of sets containing , stable by union and set difference. It is then also stable by intersection (see IsSetRing.inter_mem).

        Instances For
          theorem MeasureTheory.IsSetRing.union_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetRing C) ⦃s : Set α ⦃t : Set α :
          s Ct Cs t C
          theorem MeasureTheory.IsSetRing.diff_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetRing C) ⦃s : Set α ⦃t : Set α :
          s Ct Cs \ t C
          theorem MeasureTheory.IsSetRing.inter_mem {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetRing C) (hs : s C) (ht : t C) :
          s t C
          theorem MeasureTheory.IsSetRing.biUnion_mem {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} (hC : MeasureTheory.IsSetRing C) {s : ιSet α} (S : Finset ι) (hs : nS, s n C) :
          iS, s i C
          theorem MeasureTheory.IsSetRing.biInter_mem {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} (hC : MeasureTheory.IsSetRing C) {s : ιSet α} (S : Finset ι) (hS : S.Nonempty) (hs : nS, s n C) :
          iS, s i C
          theorem MeasureTheory.IsSetRing.partialSups_mem {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetRing C) {s : Set α} (hs : ∀ (n : ), s n C) (n : ) :
          theorem MeasureTheory.IsSetRing.disjointed_mem {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetRing C) {s : Set α} (hs : ∀ (n : ), s n C) (n : ) :