# mathlibdocumentation

measure_theory.pi_system

# 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 is_pi_system, 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 dynkin_system, 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.

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

• generate_from_generate_pi_system_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_generate_pi_system_Union_elim and mem_generate_pi_system_Union_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.

## Implementation details #

• is_pi_system 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 is_pi_system.
def is_pi_system {α : Type u_1} (C : set (set α)) :
Prop

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
theorem is_pi_system.singleton {α : Type u_1} (S : set α) :
inductive generate_pi_system {α : Type u_1} (S : set (set α)) :
set (set α)
• base : ∀ {α : Type u_1} (S : set (set α)) {s : set α}, s S
• inter : ∀ {α : Type u_1} (S : set (set α)) {s t : set α}, (s t).nonempty (s t)

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

theorem is_pi_system_generate_pi_system {α : Type u_1} (S : set (set α)) :
theorem subset_generate_pi_system_self {α : Type u_1} (S : set (set α)) :
theorem generate_pi_system_subset_self {α : Type u_1} {S : set (set α)} (h_S : is_pi_system S) :
theorem generate_pi_system_eq {α : Type u_1} {S : set (set α)} (h_pi : is_pi_system S) :
theorem generate_pi_system_mono {α : Type u_1} {S T : set (set α)} (hST : S T) :
theorem generate_pi_system_measurable_set {α : Type u_1} [M : measurable_space α] {S : set (set α)} (h_meas_S : ∀ (s : set α), s S) (t : set α) (h_in_pi : t ) :
theorem generate_from_measurable_set_of_generate_pi_system {α : Type u_1} {g : set (set α)} (t : set α) (ht : t ) :
theorem generate_from_generate_pi_system_eq {α : Type u_1} {g : set (set α)} :
theorem mem_generate_pi_system_Union_elim {α : Type u_1} {β : Type u_2} {g : β → set (set α)} (h_pi : ∀ (b : β), is_pi_system (g b)) (t : set α) (h_t : t generate_pi_system (⋃ (b : β), g b)) :
∃ (T : finset β) (f : β → set α), (t = ⋂ (b : β) (H : b T), f b) ∀ (b : β), b Tf b g b
theorem mem_generate_pi_system_Union_elim' {α : Type u_1} {β : Type u_2} {g : β → set (set α)} {s : set β} (h_pi : ∀ (b : β), b sis_pi_system (g b)) (t : set α) (h_t : t generate_pi_system (⋃ (b : β) (H : b s), g b)) :
∃ (T : finset β) (f : β → set α), T s (t = ⋂ (b : β) (H : b T), f b) ∀ (b : β), b Tf b g b
structure measurable_space.dynkin_system (α : 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".

@[ext]
theorem measurable_space.dynkin_system.ext {α : Type u_1} {d₁ d₂ : measurable_space.dynkin_system α} :
(∀ (s : set α), d₁.has s d₂.has s)d₁ = d₂
theorem measurable_space.dynkin_system.has_compl_iff {α : Type u_1} {a : set α} :
d.has a d.has a
theorem measurable_space.dynkin_system.has_univ {α : Type u_1}  :
theorem measurable_space.dynkin_system.has_Union {α : Type u_1} {β : Type u_2} [encodable β] {f : β → set α} (hd : pairwise (disjoint on f)) (h : ∀ (i : β), d.has (f i)) :
d.has (⋃ (i : β), f i)
theorem measurable_space.dynkin_system.has_union {α : Type u_1} {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₁ s₂ ) :
d.has (s₁ s₂)
theorem measurable_space.dynkin_system.has_diff {α : Type u_1} {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₂ s₁) :
d.has (s₁ \ s₂)
@[instance]
Equations

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

Equations
inductive measurable_space.dynkin_system.generate_has {α : Type u_1} (s : set (set α)) :
set α → Prop
• basic : ∀ {α : Type u_1} (s : set (set α)) (t : set α),
• empty : ∀ {α : Type u_1} (s : set (set α)),
• compl : ∀ {α : Type u_1} (s : set (set α)) {a : set α},
• Union : ∀ {α : Type u_1} (s : set (set α)) {f : set α}, pairwise (disjoint on f)(∀ (i : ), (⋃ (i : ), f i)

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

theorem measurable_space.dynkin_system.generate_has_compl {α : Type u_1} {C : set (set α)} {s : set α} :
def measurable_space.dynkin_system.generate {α : Type u_1} (s : set (set α)) :

The least Dynkin system containing a collection of basic sets.

Equations
theorem measurable_space.dynkin_system.generate_has_def {α : Type u_1} {C : set (set α)} :
@[instance]
Equations
def measurable_space.dynkin_system.to_measurable_space {α : Type u_1} (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
theorem measurable_space.dynkin_system.of_measurable_space_to_measurable_space {α : Type u_1} (h_inter : ∀ (s₁ s₂ : set α), d.has s₁d.has s₂d.has (s₁ s₂)) :
def measurable_space.dynkin_system.restrict_on {α : Type u_1} {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
theorem measurable_space.dynkin_system.generate_le {α : Type u_1} {s : set (set α)} (h : ∀ (t : set α), t sd.has t) :
theorem measurable_space.dynkin_system.generate_has_subset_generate_measurable {α : Type u_1} {C : set (set α)} {s : set α} (hs : s) :
theorem measurable_space.dynkin_system.generate_inter {α : Type u_1} {s : set (set α)} (hs : is_pi_system s) {t₁ t₂ : set α} (ht₁ : t₁) (ht₂ : t₂) :
(t₁ t₂)
theorem measurable_space.dynkin_system.generate_from_eq {α : Type u_1} {s : set (set α)} (hs : is_pi_system s) :

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 additionnally that is is non-empty, but we drop this condition in the formalization).

theorem measurable_space.induction_on_inter {α : Type u_1} {C : set α → Prop} {s : set (set α)} [m : measurable_space α] (h_eq : m = ) (h_inter : is_pi_system s) (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 : ), measurable_set (f i))(∀ (i : ), C (f i))C (⋃ (i : ), f i)) ⦃t : set α⦄ :
C t