# Documentation

Mathlib.MeasureTheory.PiSystem

# 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.

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 | t, 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 => 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 : α} → 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 | l, l s u, u t 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 : α} → 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 | 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 | l, l s u, u t l < u Set.Ioo l u = S}
theorem isPiSystem_Ioo {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] (f : ια) (g : ι'α) :
IsPiSystem {S | 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 | l, l s u, u t l < u Set.Ioc l u = S}
theorem isPiSystem_Ioc {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] (f : ια) (g : ι'α) :
IsPiSystem {S | 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 | l, l s u, u t l < u Set.Ico l u = S}
theorem isPiSystem_Ico {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] (f : ια) (g : ι'α) :
IsPiSystem {S | 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 | l, l s u, u t l u Set.Icc l u = S}
theorem isPiSystem_Icc {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [] (f : ια) (g : ι'α) :
IsPiSystem {S | 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 : ∀ (s : Set α), s S) (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, t = ⋂ (b : β) (_ : b T), f b ∀ (b : β), b Tf b g b
theorem mem_generatePiSystem_iUnion_elim' {α : Type u_1} {β : Type u_2} {g : βSet (Set α)} {s : Set β} (h_pi : ∀ (b : β), b sIsPiSystem (g b)) (t : Set α) (h_t : t generatePiSystem (⋃ (b : β) (_ : b s), g b)) :
T f, T s t = ⋂ (b : β) (_ : b T), f b ∀ (b : β), b Tf 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.

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' | t x, s' = ⋂ (i : ι) (_ : i t), s i}
theorem generateFrom_piiUnionInter_singleton_left {α : Type u_1} {ι : Type u_2} (s : ιSet α) (S : Set ι) :
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 | }) 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 | }) S) :
theorem generateFrom_piiUnionInter_measurableSet {α : Type u_1} {ι : Type u_2} (m : ι) (S : Set ι) :
MeasurableSpace.generateFrom (piiUnionInter (fun n => {s | }) S) = ⨆ (i : ι) (_ : i S), m i

## Dynkin systems and Π-λ theorem #

structure MeasurableSpace.DynkinSystem (α : Type u_2) :
Type u_2
• Has : Set αProp

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

• has_empty :

A Dynkin system contains the empty set.

• has_compl : ∀ {a : Set α},

A Dynkin system is closed under complementation.

• has_iUnion_nat : ∀ {f : Set α}, Pairwise (Disjoint on f)(∀ (i : ), ) → MeasurableSpace.DynkinSystem.Has s (⋃ (i : ), f i)

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

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".

Instances For
theorem MeasurableSpace.DynkinSystem.ext {α : Type u_1} {d₁ : } {d₂ : } :
(∀ (s : Set α), ) → d₁ = d₂
theorem MeasurableSpace.DynkinSystem.has_compl_iff {α : Type u_1} (d : ) {a : Set α} :
theorem MeasurableSpace.DynkinSystem.has_iUnion {α : Type u_1} (d : ) {β : Type u_2} [] {f : βSet α} (hd : Pairwise (Disjoint on f)) (h : ∀ (i : β), ) :
MeasurableSpace.DynkinSystem.Has d (⋃ (i : β), f i)
theorem MeasurableSpace.DynkinSystem.has_union {α : Type u_1} (d : ) {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) (h : Disjoint s₁ s₂) :
theorem MeasurableSpace.DynkinSystem.has_diff {α : Type u_1} (d : ) {s₁ : Set α} {s₂ : Set α} (h₁ : ) (h₂ : ) (h : s₂ s₁) :
theorem MeasurableSpace.DynkinSystem.le_def {α : Type u_2} {a : } {b : } :
a b a.Has b.Has

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

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.

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

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

Instances For
theorem MeasurableSpace.DynkinSystem.ofMeasurableSpace_toMeasurableSpace {α : Type u_1} (d : ) (h_inter : ∀ (s₁ s₂ : Set α), MeasurableSpace.DynkinSystem.Has d (s₁ s₂)) :
def MeasurableSpace.DynkinSystem.restrictOn {α : Type u_1} (d : ) {s : Set α} (h : ) :

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

Instances For
theorem MeasurableSpace.DynkinSystem.generate_le {α : Type u_1} (d : ) {s : Set (Set α)} (h : ∀ (t : Set α), t s) :
theorem MeasurableSpace.DynkinSystem.generate_inter {α : Type u_1} {s : Set (Set α)} (hs : ) {t₁ : Set α} {t₂ : Set α} :
theorem MeasurableSpace.DynkinSystem.generateFrom_eq {α : Type u_1} {s : Set (Set α)} (hs : ) :
= MeasurableSpace.DynkinSystem.toMeasurableSpace () (_ : ∀ (t₁ t₂ : Set α), )

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 : (t : Set α) → t sC 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