mathlib documentation

measure_theory.pi_system

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

Main statements #

Implementation details #

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 α) :
theorem is_pi_system.insert_empty {α : Type u_1} {S : set (set α)} (h_pi : is_pi_system S) :
theorem is_pi_system.comap {α : Type u_1} {β : Type u_2} {S : set (set β)} (h_pi : is_pi_system S) (f : α β) :
is_pi_system {s : set α | (t : set β) (H : t S), f ⁻¹' t = s}
theorem is_pi_system_Union_of_directed_le {α : Type u_1} {ι : Sort u_2} (p : ι set (set α)) (hp_pi : (n : ι), is_pi_system (p n)) (hp_directed : directed has_le.le p) :
is_pi_system ( (n : ι), p n)
theorem is_pi_system_Union_of_monotone {α : Type u_1} {ι : Type u_2} [semilattice_sup ι] (p : ι set (set α)) (hp_pi : (n : ι), is_pi_system (p n)) (hp_mono : monotone p) :
is_pi_system ( (n : ι), p n)
theorem is_pi_system_image_Iio {α : Type u_1} [linear_order α] (s : set α) :
theorem is_pi_system_image_Ioi {α : Type u_1} [linear_order α] (s : set α) :
theorem is_pi_system_Ixx_mem {α : Type u_1} [linear_order α] {Ixx : α α set α} {p : α α Prop} (Hne : {a b : α}, (Ixx a b).nonempty p a b) (Hi : {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ Ixx a₂ b₂ = Ixx (linear_order.max a₁ a₂) (linear_order.min b₁ b₂)) (s t : set α) :
is_pi_system {S : set α | (l : α) (H : l s) (u : α) (H : u t) (hlu : p l u), Ixx l u = S}
theorem is_pi_system_Ixx {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [linear_order α] {Ixx : α α set α} {p : α α Prop} (Hne : {a b : α}, (Ixx a b).nonempty p a b) (Hi : {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ Ixx a₂ b₂ = Ixx (linear_order.max a₁ a₂) (linear_order.min b₁ b₂)) (f : ι α) (g : ι' α) :
is_pi_system {S : set α | (i : ι) (j : ι') (h : p (f i) (g j)), Ixx (f i) (g j) = S}
theorem is_pi_system_Ioo_mem {α : Type u_1} [linear_order α] (s t : set α) :
is_pi_system {S : set α | (l : α) (H : l s) (u : α) (H : u t) (h : l < u), set.Ioo l u = S}
theorem is_pi_system_Ioo {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [linear_order α] (f : ι α) (g : ι' α) :
is_pi_system {S : set α | (l : ι) (u : ι') (h : f l < g u), set.Ioo (f l) (g u) = S}
theorem is_pi_system_Ioc_mem {α : Type u_1} [linear_order α] (s t : set α) :
is_pi_system {S : set α | (l : α) (H : l s) (u : α) (H : u t) (h : l < u), set.Ioc l u = S}
theorem is_pi_system_Ioc {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [linear_order α] (f : ι α) (g : ι' α) :
is_pi_system {S : set α | (i : ι) (j : ι') (h : f i < g j), set.Ioc (f i) (g j) = S}
theorem is_pi_system_Ico_mem {α : Type u_1} [linear_order α] (s t : set α) :
is_pi_system {S : set α | (l : α) (H : l s) (u : α) (H : u t) (h : l < u), set.Ico l u = S}
theorem is_pi_system_Ico {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [linear_order α] (f : ι α) (g : ι' α) :
is_pi_system {S : set α | (i : ι) (j : ι') (h : f i < g j), set.Ico (f i) (g j) = S}
theorem is_pi_system_Icc_mem {α : Type u_1} [linear_order α] (s t : set α) :
is_pi_system {S : set α | (l : α) (H : l s) (u : α) (H : u t) (h : l u), set.Icc l u = S}
theorem is_pi_system_Icc {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [linear_order α] (f : ι α) (g : ι' α) :
is_pi_system {S : set α | (i : ι) (j : ι') (h : f i g j), set.Icc (f i) (g j) = S}
inductive generate_pi_system {α : Type u_1} (S : set (set α)) :
set (set α)

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

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 measurable_set s) (t : set α) (h_in_pi : t generate_pi_system S) :
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 T f 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 s is_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 T f b g b

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

def pi_Union_Inter {α : 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
theorem pi_Union_Inter_singleton {α : Type u_1} {ι : Type u_2} (π : ι set (set α)) (i : ι) :
theorem pi_Union_Inter_singleton_left {α : Type u_1} {ι : Type u_2} (s : ι set α) (S : set ι) :
pi_Union_Inter (λ (i : ι), {s i}) S = {s' : set α | (t : finset ι) (htS : t S), s' = (i : ι) (H : i t), s i}
theorem generate_from_pi_Union_Inter_singleton_left {α : Type u_1} {ι : Type u_2} (s : ι set α) (S : set ι) :
measurable_space.generate_from (pi_Union_Inter (λ (k : ι), {s k}) S) = measurable_space.generate_from {t : set α | (k : ι) (H : k S), s k = t}
theorem is_pi_system_pi_Union_Inter {α : Type u_1} {ι : Type u_2} (π : ι set (set α)) (hpi : (x : ι), is_pi_system (π x)) (S : set ι) :

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

theorem pi_Union_Inter_mono_left {α : Type u_1} {ι : Type u_2} {π π' : ι set (set α)} (h_le : (i : ι), π i π' i) (S : set ι) :
theorem pi_Union_Inter_mono_right {α : Type u_1} {ι : Type u_2} {π : ι set (set α)} {S T : set ι} (hST : S T) :
theorem generate_from_pi_Union_Inter_le {α : Type u_1} {ι : Type u_2} {m : measurable_space α} (π : ι set (set α)) (h : (n : ι), measurable_space.generate_from (π n) m) (S : set ι) :
theorem subset_pi_Union_Inter {α : Type u_1} {ι : Type u_2} {π : ι set (set α)} {S : set ι} {i : ι} (his : i S) :
theorem mem_pi_Union_Inter_of_measurable_set {α : Type u_1} {ι : Type u_2} (m : ι measurable_space α) {S : set ι} {i : ι} (hiS : i S) (s : set α) (hs : measurable_set s) :
s pi_Union_Inter (λ (n : ι), {s : set α | measurable_set s}) S
theorem le_generate_from_pi_Union_Inter {α : Type u_1} {ι : Type u_2} {π : ι set (set α)} (S : set ι) {x : ι} (hxS : x S) :
theorem measurable_set_supr_of_mem_pi_Union_Inter {α : Type u_1} {ι : Type u_2} (m : ι measurable_space α) (S : set ι) (t : set α) (ht : t pi_Union_Inter (λ (n : ι), {s : set α | measurable_set s}) S) :
theorem generate_from_pi_Union_Inter_measurable_set {α : Type u_1} {ι : Type u_2} (m : ι measurable_space α) (S : set ι) :
measurable_space.generate_from (pi_Union_Inter (λ (n : ι), {s : set α | measurable_set s}) S) = (i : ι) (H : i S), m i

Dynkin systems and Π-λ theorem #

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

Instances for measurable_space.dynkin_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_Union {α : Type u_1} (d : measurable_space.dynkin_system α) {β : Type u_2} [countable β] {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} (d : measurable_space.dynkin_system α) {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : disjoint s₁ s₂) :
d.has (s₁ s₂)
theorem measurable_space.dynkin_system.has_diff {α : Type u_1} (d : measurable_space.dynkin_system α) {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₂ s₁) :
d.has (s₁ \ s₂)
inductive measurable_space.dynkin_system.generate_has {α : 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.

The least Dynkin system containing a collection of basic sets.

Equations
def measurable_space.dynkin_system.to_measurable_space {α : Type u_1} (d : measurable_space.dynkin_system α) (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

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

Equations

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 = measurable_space.generate_from s) (h_inter : is_pi_system s) (h_empty : C ) (h_basic : (t : set α), t s C t) (h_compl : (t : set α), measurable_set t C t C t) (h_union : (f : set α), pairwise (disjoint on f) ( (i : ), measurable_set (f i)) ( (i : ), C (f i)) C ( (i : ), f i)) ⦃t : set α⦄ :