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

## Main statements #

• The main theorem of this file is Dynkin's π-λ theorem, which appears here as an induction principle induction_on_inter. Suppose s is a collection of subsets of α such that the intersection of two members of s belongs to s whenever it is nonempty. Let m be the σ-algebra generated by s. In order to check that a predicate C holds on every member of m, it suffices to check that C holds on the members of s and that C is preserved by complementation and disjoint countable unions.

• The proof of this theorem relies on the notion of IsPiSystem, i.e., a collection of sets which is closed under binary non-empty intersections. Note that this is a small variation around the usual notion in the literature, which often requires that a π-system is non-empty, and closed also under disjoint intersections. This variation turns out to be convenient for the formalization.

• The proof of Dynkin's π-λ theorem also requires the notion of DynkinSystem, i.e., a collection of sets which 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.

• generatePiSystem g gives the minimal π-system containing g. This can be considered a Galois insertion into both measurable spaces and sets.

• generateFrom_generatePiSystem_eq proves that if you start from a collection of sets g, take the generated π-system, and then the generated σ-algebra, you get the same result as the σ-algebra generated from g. This is useful because there are connections between independent sets that are π-systems and the generated independent spaces.

• mem_generatePiSystem_iUnion_elim and mem_generatePiSystem_iUnion_elim' show that any element of the π-system generated from the union of a set of π-systems can be represented as the intersection of a finite number of elements from these sets.

• piiUnionInter defines a new π-system from a family of π-systems π : ι → Set (Set α) and a set of indices S : Set ι. piiUnionInter π S is the set of sets that can be written as ⋂ x ∈ t, f x for some finset t ∈ S and sets f x ∈ π x.

## Implementation details #

• IsPiSystem is a predicate, not a type. Thus, we don't explicitly define the galois insertion, nor do we define a complete lattice. In theory, we could define a complete lattice and galois insertion on the subtype corresponding to IsPiSystem.
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
• = sC, tC, (s t).Nonemptys t C
Instances For
theorem IsPiSystem.singleton {α : Type u_1} (S : Set α) :
theorem IsPiSystem.insert_empty {α : Type u_1} {S : Set (Set α)} (h_pi : ) :
theorem IsPiSystem.insert_univ {α : Type u_1} {S : Set (Set α)} (h_pi : ) :
IsPiSystem (insert Set.univ S)
theorem IsPiSystem.comap {α : Type u_1} {β : Type u_2} {S : Set (Set β)} (h_pi : ) (f : αβ) :
IsPiSystem {s : Set α | tS, 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} [] (p : ιSet (Set α)) (hp_pi : ∀ (n : ι), IsPiSystem (p n)) (hp_mono : ) :
IsPiSystem (⋃ (n : ι), p n)
theorem isPiSystem_image_Iio {α : Type u_1} [] (s : Set α) :
IsPiSystem (Set.Iio '' s)
theorem isPiSystem_Iio {α : Type u_1} [] :
theorem isPiSystem_image_Ioi {α : Type u_1} [] (s : Set α) :
IsPiSystem (Set.Ioi '' s)
theorem isPiSystem_Ioi {α : Type u_1} [] :
theorem isPiSystem_image_Iic {α : Type u_1} [] (s : Set α) :
IsPiSystem (Set.Iic '' s)
theorem isPiSystem_Iic {α : Type u_1} [] :
theorem isPiSystem_image_Ici {α : Type u_1} [] (s : Set α) :
IsPiSystem (Set.Ici '' s)
theorem isPiSystem_Ici {α : Type u_1} [] :
theorem isPiSystem_Ixx_mem {α : Type u_1} [] {Ixx : ααSet α} {p : ααProp} (Hne : ∀ {a b : α}, (Ixx a b).Nonemptyp 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 α | ls, ut, p l u Ixx l u = S}
theorem isPiSystem_Ixx {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] {Ixx : ααSet α} {p : ααProp} (Hne : ∀ {a b : α}, (Ixx a b).Nonemptyp 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} [] (s : Set α) (t : Set α) :
IsPiSystem {S : Set α | ls, ut, l < u Set.Ioo l u = S}
theorem isPiSystem_Ioo {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] (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} [] (s : Set α) (t : Set α) :
IsPiSystem {S : Set α | ls, ut, l < u Set.Ioc l u = S}
theorem isPiSystem_Ioc {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] (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} [] (s : Set α) (t : Set α) :
IsPiSystem {S : Set α | ls, ut, l < u Set.Ico l u = S}
theorem isPiSystem_Ico {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] (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} [] (s : Set α) (t : Set α) :
IsPiSystem {S : Set α | ls, ut, l u Set.Icc l u = S}
theorem isPiSystem_Icc {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] (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 isPiSystem_generatePiSystem {α : Type u_1} (S : Set (Set α)) :
theorem subset_generatePiSystem_self {α : Type u_1} (S : Set (Set α)) :
theorem generatePiSystem_subset_self {α : Type u_1} {S : Set (Set α)} (h_S : ) :
theorem generatePiSystem_eq {α : Type u_1} {S : Set (Set α)} (h_pi : ) :
theorem generatePiSystem_mono {α : Type u_1} {S : Set (Set α)} {T : Set (Set α)} (hST : S T) :
theorem generatePiSystem_measurableSet {α : Type u_1} [M : ] {S : Set (Set α)} (h_meas_S : sS, ) (t : Set α) (h_in_pi : ) :
theorem generateFrom_measurableSet_of_generatePiSystem {α : Type u_1} {g : Set (Set α)} (t : Set α) (ht : ) :
theorem generateFrom_generatePiSystem_eq {α : Type u_1} {g : Set (Set α)} :
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 : ) (f : βSet α), t = bT, f b bT, f b g b

Every element of the π-system generated by the union of a family of π-systems is a finite intersection of elements from the π-systems. For an indexed union version, see mem_generatePiSystem_iUnion_elim'.

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 (bs, g b)) :
∃ (T : ) (f : βSet α), T s t = bT, f b bT, f b g b

Every element of the π-system generated by an indexed union of a family of π-systems is a finite intersection of elements from the π-systems. For a total union version, see mem_generatePiSystem_iUnion_elim.

### π-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
• = {s : Set α | ∃ (t : ) (_ : t S) (f : ιSet α) (_ : xt, f x π x), s = xt, f x}
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 : ) (_ : t S), s' = it, 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 α | kS, 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 : } (π : ιSet (Set α)) (h : ∀ (n : ι), ) (S : Set ι) :
theorem subset_piiUnionInter {α : Type u_1} {ι : Type u_2} {π : ιSet (Set α)} {S : Set ι} {i : ι} (his : i S) :
π i
theorem mem_piiUnionInter_of_measurableSet {α : Type u_1} {ι : Type u_2} (m : ι) {S : Set ι} {i : ι} (hiS : i S) (s : Set α) (hs : ) :
s piiUnionInter (fun (n : ι) => {s : Set α | }) 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 : ι) (S : Set ι) (t : Set α) (ht : t piiUnionInter (fun (n : ι) => {s : Set α | }) S) :
theorem generateFrom_piiUnionInter_measurableSet {α : Type u_1} {ι : Type u_2} (m : ι) (S : Set ι) :
MeasurableSpace.generateFrom (piiUnionInter (fun (n : ι) => {s : Set α | }) S) = iS, 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.has_empty {α : Type u_2} (self : ) :
self.Has

A Dynkin system contains the empty set.

theorem MeasurableSpace.DynkinSystem.has_compl {α : Type u_2} (self : ) {a : Set α} :
self.Has aself.Has a

A Dynkin system is closed under complementation.

theorem MeasurableSpace.DynkinSystem.has_iUnion_nat {α : Type u_2} (self : ) {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.

theorem MeasurableSpace.DynkinSystem.ext {α : Type u_1} {d₁ : } {d₂ : } :
(∀ (s : Set α), d₁.Has s d₂.Has s)d₁ = d₂
theorem MeasurableSpace.DynkinSystem.has_compl_iff {α : Type u_1} (d : ) {a : Set α} :
d.Has a d.Has a
theorem MeasurableSpace.DynkinSystem.has_univ {α : Type u_1} (d : ) :
d.Has Set.univ
theorem MeasurableSpace.DynkinSystem.has_iUnion {α : Type u_1} (d : ) {β : Type u_2} [] {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 : ) {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 : ) {s₁ : Set α} {s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h : s₂ s₁) :
d.Has (s₁ \ s₂)
Equations
• MeasurableSpace.DynkinSystem.instLEDynkinSystem = { le := fun (m₁ m₂ : ) => m₁.Has m₂.Has }
theorem MeasurableSpace.DynkinSystem.le_def {α : Type u_2} {a : } {b : } :
a b a.Has b.Has
Equations
• MeasurableSpace.DynkinSystem.instPartialOrder = let __src := MeasurableSpace.DynkinSystem.instLEDynkinSystem;

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

Equations
• = { Has := m.MeasurableSet', has_empty := , has_compl := , has_iUnion_nat := }
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
theorem MeasurableSpace.DynkinSystem.generateHas_compl {α : Type u_1} {C : Set (Set α)} {s : Set α} :

The least Dynkin system containing a collection of basic sets.

Equations
• = { Has := , has_empty := , has_compl := , has_iUnion_nat := }
Instances For
Equations
• MeasurableSpace.DynkinSystem.instInhabited = { default := }
def MeasurableSpace.DynkinSystem.toMeasurableSpace {α : Type u_1} (d : ) (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
• d.toMeasurableSpace h_inter = { MeasurableSet' := d.Has, measurableSet_empty := , measurableSet_compl := , measurableSet_iUnion := }
Instances For
theorem MeasurableSpace.DynkinSystem.ofMeasurableSpace_toMeasurableSpace {α : Type u_1} (d : ) (h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁d.Has s₂d.Has (s₁ s₂)) :
MeasurableSpace.DynkinSystem.ofMeasurableSpace (d.toMeasurableSpace h_inter) = d
def MeasurableSpace.DynkinSystem.restrictOn {α : Type u_1} (d : ) {s : Set α} (h : d.Has s) :

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

Equations
• d.restrictOn h = { Has := fun (t : Set α) => d.Has (t s), has_empty := , has_compl := , has_iUnion_nat := }
Instances For
theorem MeasurableSpace.DynkinSystem.generate_le {α : Type u_1} (d : ) {s : Set (Set α)} (h : ts, d.Has t) :
theorem MeasurableSpace.DynkinSystem.generate_inter {α : Type u_1} {s : Set (Set α)} (hs : ) {t₁ : Set α} {t₂ : Set α} (ht₁ : t₁) (ht₂ : t₂) :
(t₁ t₂)
theorem MeasurableSpace.DynkinSystem.generateFrom_eq {α : Type u_1} {s : Set (Set α)} (hs : ) :
= .toMeasurableSpace

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 : ] (h_eq : ) (h_inter : ) (h_empty : C ) (h_basic : ts, C t) (h_compl : ∀ (t : Set α), C tC t) (h_union : ∀ (f : Set α), Pairwise (Disjoint on f)(∀ (i : ), MeasurableSet (f i))(∀ (i : ), C (f i))C (⋃ (i : ), f i)) ⦃t : Set α :
C t