Documentation

Mathlib.MeasureTheory.PiSystem

Induction principles for measurable sets, related to π-systems and λ-systems. #

Main statements #

Implementation details #

def IsPiSystem {α : Type u_1} (C : Set (Set α)) :

A π-system is a collection of subsets of α that is closed under binary intersection of non-disjoint sets. Usually it is also required that the collection is nonempty, but we don't do that here.

Equations
Instances For
    theorem IsPiSystem.singleton {α : Type u_1} (S : Set α) :
    theorem IsPiSystem.insert_empty {α : Type u_1} {S : Set (Set α)} (h_pi : IsPiSystem S) :
    theorem IsPiSystem.insert_univ {α : Type u_1} {S : Set (Set α)} (h_pi : IsPiSystem S) :
    IsPiSystem (insert Set.univ S)
    theorem IsPiSystem.comap {α : Type u_1} {β : Type u_2} {S : Set (Set β)} (h_pi : IsPiSystem S) (f : αβ) :
    IsPiSystem {s : Set α | ∃ t ∈ S, f ⁻¹' t = s}
    theorem isPiSystem_iUnion_of_directed_le {α : Type u_1} {ι : Sort u_2} (p : ιSet (Set α)) (hp_pi : ∀ (n : ι), IsPiSystem (p n)) (hp_directed : Directed (fun (x x_1 : Set (Set α)) => x x_1) p) :
    IsPiSystem (⋃ (n : ι), p n)
    theorem isPiSystem_iUnion_of_monotone {α : Type u_1} {ι : Type u_2} [SemilatticeSup ι] (p : ιSet (Set α)) (hp_pi : ∀ (n : ι), IsPiSystem (p n)) (hp_mono : Monotone p) :
    IsPiSystem (⋃ (n : ι), p n)
    theorem isPiSystem_image_Iio {α : Type u_1} [LinearOrder α] (s : Set α) :
    IsPiSystem (Set.Iio '' s)
    theorem isPiSystem_Iio {α : Type u_1} [LinearOrder α] :
    theorem isPiSystem_image_Ioi {α : Type u_1} [LinearOrder α] (s : Set α) :
    IsPiSystem (Set.Ioi '' s)
    theorem isPiSystem_Ioi {α : Type u_1} [LinearOrder α] :
    theorem isPiSystem_image_Iic {α : Type u_1} [LinearOrder α] (s : Set α) :
    IsPiSystem (Set.Iic '' s)
    theorem isPiSystem_Iic {α : Type u_1} [LinearOrder α] :
    theorem isPiSystem_image_Ici {α : Type u_1} [LinearOrder α] (s : Set α) :
    IsPiSystem (Set.Ici '' s)
    theorem isPiSystem_Ici {α : Type u_1} [LinearOrder α] :
    theorem isPiSystem_Ixx_mem {α : Type u_1} [LinearOrder α] {Ixx : ααSet α} {p : ααProp} (Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b)p a b) (Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) (s : Set α) (t : Set α) :
    IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, p l u Ixx l u = S}
    theorem isPiSystem_Ixx {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [LinearOrder α] {Ixx : ααSet α} {p : ααProp} (Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b)p a b) (Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) (f : ια) (g : ι'α) :
    IsPiSystem {S : Set α | ∃ (i : ι) (j : ι'), p (f i) (g j) Ixx (f i) (g j) = S}
    theorem isPiSystem_Ioo_mem {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) :
    IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u Set.Ioo l u = S}
    theorem isPiSystem_Ioo {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [LinearOrder α] (f : ια) (g : ι'α) :
    IsPiSystem {S : Set α | ∃ (l : ι) (u : ι'), f l < g u Set.Ioo (f l) (g u) = S}
    theorem isPiSystem_Ioc_mem {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) :
    IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u Set.Ioc l u = S}
    theorem isPiSystem_Ioc {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [LinearOrder α] (f : ια) (g : ι'α) :
    IsPiSystem {S : Set α | ∃ (i : ι) (j : ι'), f i < g j Set.Ioc (f i) (g j) = S}
    theorem isPiSystem_Ico_mem {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) :
    IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l < u Set.Ico l u = S}
    theorem isPiSystem_Ico {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [LinearOrder α] (f : ια) (g : ι'α) :
    IsPiSystem {S : Set α | ∃ (i : ι) (j : ι'), f i < g j Set.Ico (f i) (g j) = S}
    theorem isPiSystem_Icc_mem {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) :
    IsPiSystem {S : Set α | ∃ l ∈ s, ∃ u ∈ t, l u Set.Icc l u = S}
    theorem isPiSystem_Icc {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [LinearOrder α] (f : ια) (g : ι'α) :
    IsPiSystem {S : Set α | ∃ (i : ι) (j : ι'), f i g j Set.Icc (f i) (g j) = S}
    inductive generatePiSystem {α : Type u_1} (S : Set (Set α)) :
    Set (Set α)

    Given a collection S of subsets of α, then generatePiSystem S is the smallest π-system containing S.

    Instances For
      theorem generatePiSystem_subset_self {α : Type u_1} {S : Set (Set α)} (h_S : IsPiSystem S) :
      theorem generatePiSystem_eq {α : Type u_1} {S : Set (Set α)} (h_pi : IsPiSystem S) :
      theorem generatePiSystem_mono {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (hST : S T) :
      theorem generatePiSystem_measurableSet {α : Type u_1} [M : MeasurableSpace α] {S : Set (Set α)} (h_meas_S : sS, MeasurableSet s) (t : Set α) (h_in_pi : t generatePiSystem S) :
      theorem mem_generatePiSystem_iUnion_elim {α : Type u_1} {β : Type u_2} {g : βSet (Set α)} (h_pi : ∀ (b : β), IsPiSystem (g b)) (t : Set α) (h_t : t generatePiSystem (⋃ (b : β), g b)) :
      ∃ (T : Finset β) (f : βSet α), t = ⋂ b ∈ T, f b bT, f b g b
      theorem mem_generatePiSystem_iUnion_elim' {α : Type u_1} {β : Type u_2} {g : βSet (Set α)} {s : Set β} (h_pi : bs, IsPiSystem (g b)) (t : Set α) (h_t : t generatePiSystem (⋃ b ∈ s, g b)) :
      ∃ (T : Finset β) (f : βSet α), T s t = ⋂ b ∈ T, f b bT, f b g b

      π-system generated by finite intersections of sets of a π-system family #

      def piiUnionInter {α : Type u_1} {ι : Type u_2} (π : ιSet (Set α)) (S : Set ι) :
      Set (Set α)

      From a set of indices S : Set ι and a family of sets of sets π : ι → Set (Set α), define the set of sets that can be written as ⋂ x ∈ t, f x for some finset t ⊆ S and sets f x ∈ π x. If π is a family of π-systems, then it is a π-system.

      Equations
      Instances For
        theorem piiUnionInter_singleton {α : Type u_1} {ι : Type u_2} (π : ιSet (Set α)) (i : ι) :
        piiUnionInter π {i} = π i {Set.univ}
        theorem piiUnionInter_singleton_left {α : Type u_1} {ι : Type u_2} (s : ιSet α) (S : Set ι) :
        piiUnionInter (fun (i : ι) => {s i}) S = {s' : Set α | ∃ (t : Finset ι) (_ : t S), s' = ⋂ i ∈ t, s i}
        theorem generateFrom_piiUnionInter_singleton_left {α : Type u_1} {ι : Type u_2} (s : ιSet α) (S : Set ι) :
        MeasurableSpace.generateFrom (piiUnionInter (fun (k : ι) => {s k}) S) = MeasurableSpace.generateFrom {t : Set α | ∃ k ∈ S, s k = t}
        theorem isPiSystem_piiUnionInter {α : Type u_1} {ι : Type u_2} (π : ιSet (Set α)) (hpi : ∀ (x : ι), IsPiSystem (π x)) (S : Set ι) :

        If π is a family of π-systems, then piiUnionInter π S is a π-system.

        theorem piiUnionInter_mono_left {α : Type u_1} {ι : Type u_2} {π : ιSet (Set α)} {π' : ιSet (Set α)} (h_le : ∀ (i : ι), π i π' i) (S : Set ι) :
        theorem piiUnionInter_mono_right {α : Type u_1} {ι : Type u_2} {π : ιSet (Set α)} {S : Set ι} {T : Set ι} (hST : S T) :
        theorem generateFrom_piiUnionInter_le {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} (π : ιSet (Set α)) (h : ∀ (n : ι), MeasurableSpace.generateFrom (π n) m) (S : Set ι) :
        theorem subset_piiUnionInter {α : Type u_1} {ι : Type u_2} {π : ιSet (Set α)} {S : Set ι} {i : ι} (his : i S) :
        π i piiUnionInter π S
        theorem mem_piiUnionInter_of_measurableSet {α : Type u_1} {ι : Type u_2} (m : ιMeasurableSpace α) {S : Set ι} {i : ι} (hiS : i S) (s : Set α) (hs : MeasurableSet s) :
        s piiUnionInter (fun (n : ι) => {s : Set α | MeasurableSet s}) S
        theorem le_generateFrom_piiUnionInter {α : Type u_1} {ι : Type u_2} {π : ιSet (Set α)} (S : Set ι) {x : ι} (hxS : x S) :
        theorem measurableSet_iSup_of_mem_piiUnionInter {α : Type u_1} {ι : Type u_2} (m : ιMeasurableSpace α) (S : Set ι) (t : Set α) (ht : t piiUnionInter (fun (n : ι) => {s : Set α | MeasurableSet s}) S) :
        theorem generateFrom_piiUnionInter_measurableSet {α : Type u_1} {ι : Type u_2} (m : ιMeasurableSpace α) (S : Set ι) :
        MeasurableSpace.generateFrom (piiUnionInter (fun (n : ι) => {s : Set α | MeasurableSet s}) S) = ⨆ i ∈ S, m i

        Dynkin systems and Π-λ theorem #

        structure MeasurableSpace.DynkinSystem (α : Type u_2) :
        Type u_2

        A Dynkin system is a collection of subsets of a type α that contains the empty set, is closed under complementation and under countable union of pairwise disjoint sets. The disjointness condition is the only difference with σ-algebras.

        The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras generated by a collection of sets which is stable under intersection.

        A Dynkin system is also known as a "λ-system" or a "d-system".

        • Has : Set αProp

          Predicate saying that a given set is contained in the Dynkin system.

        • has_empty : self.Has

          A Dynkin system contains the empty set.

        • has_compl : ∀ {a : Set α}, self.Has aself.Has a

          A Dynkin system is closed under complementation.

        • has_iUnion_nat : ∀ {f : Set α}, Pairwise (Disjoint on f)(∀ (i : ), self.Has (f i))self.Has (⋃ (i : ), f i)

          A Dynkin system is closed under countable union of pairwise disjoint sets. Use a more general MeasurableSpace.DynkinSystem.has_iUnion instead.

        Instances For
          theorem MeasurableSpace.DynkinSystem.ext {α : Type u_1} {d₁ : MeasurableSpace.DynkinSystem α} {d₂ : MeasurableSpace.DynkinSystem α} :
          (∀ (s : Set α), d₁.Has s d₂.Has s)d₁ = d₂
          theorem MeasurableSpace.DynkinSystem.has_iUnion {α : Type u_1} (d : MeasurableSpace.DynkinSystem α) {β : Type u_2} [Countable β] {f : βSet α} (hd : Pairwise (Disjoint on f)) (h : ∀ (i : β), d.Has (f i)) :
          d.Has (⋃ (i : β), f i)
          theorem MeasurableSpace.DynkinSystem.has_union {α : Type u_1} (d : MeasurableSpace.DynkinSystem α) {s₁ : Set α} {s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h : Disjoint s₁ s₂) :
          d.Has (s₁ s₂)
          theorem MeasurableSpace.DynkinSystem.has_diff {α : Type u_1} (d : MeasurableSpace.DynkinSystem α) {s₁ : Set α} {s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h : s₂ s₁) :
          d.Has (s₁ \ s₂)
          Equations
          Equations
          • MeasurableSpace.DynkinSystem.instPartialOrderDynkinSystem = let __src := MeasurableSpace.DynkinSystem.instLEDynkinSystem; PartialOrder.mk

          Every measurable space (σ-algebra) forms a Dynkin system

          Equations
          Instances For
            inductive MeasurableSpace.DynkinSystem.GenerateHas {α : Type u_1} (s : Set (Set α)) :
            Set αProp

            The least Dynkin system containing a collection of basic sets. This inductive type gives the underlying collection of sets.

            Instances For

              The least Dynkin system containing a collection of basic sets.

              Equations
              Instances For
                Equations
                def MeasurableSpace.DynkinSystem.toMeasurableSpace {α : Type u_1} (d : MeasurableSpace.DynkinSystem α) (h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁d.Has s₂d.Has (s₁ s₂)) :

                If a Dynkin system is closed under binary intersection, then it forms a σ-algebra.

                Equations
                Instances For

                  If s is in a Dynkin system d, we can form the new Dynkin system {s ∩ t | t ∈ d}.

                  Equations
                  Instances For
                    theorem MeasurableSpace.DynkinSystem.generate_inter {α : Type u_1} {s : Set (Set α)} (hs : IsPiSystem s) {t₁ : Set α} {t₂ : Set α} (ht₁ : (MeasurableSpace.DynkinSystem.generate s).Has t₁) (ht₂ : (MeasurableSpace.DynkinSystem.generate s).Has t₂) :

                    Dynkin's π-λ theorem: Given a collection of sets closed under binary intersections, then the Dynkin system it generates is equal to the σ-algebra it generates. This result is known as the π-λ theorem. A collection of sets closed under binary intersection is called a π-system (often requiring additionally that it is non-empty, but we drop this condition in the formalization).

                    theorem MeasurableSpace.induction_on_inter {α : Type u_1} {C : Set αProp} {s : Set (Set α)} [m : MeasurableSpace α] (h_eq : m = MeasurableSpace.generateFrom s) (h_inter : IsPiSystem s) (h_empty : C ) (h_basic : ts, C t) (h_compl : ∀ (t : Set α), MeasurableSet tC tC t) (h_union : ∀ (f : Set α), Pairwise (Disjoint on f)(∀ (i : ), MeasurableSet (f i))(∀ (i : ), C (f i))C (⋃ (i : ), f i)) ⦃t : Set α :
                    MeasurableSet tC t