measure_theory.pi_system

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
pi_Union_Inter defines a new π-system from a family of π-systems π : ι → set (set α) and a set of indices S : set ι. pi_Union_Inter π 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 #

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

is_pi_system C = ∀ (s : set α), s ∈ C → ∀ (t : set α), t ∈ C → (s ∩ t).nonempty → s ∩ t ∈ C

source

theorem measurable_space.is_pi_system_measurable_set {α : Type u_1} [measurable_space α] :

is_pi_system {s : set α | measurable_set s}

source

theorem is_pi_system.singleton {α : Type u_1} (S : set α) :

is_pi_system {S}

source

theorem is_pi_system.insert_empty {α : Type u_1} {S : set (set α)} (h_pi : is_pi_system S) :

is_pi_system (has_insert.insert ∅ S)

source

theorem is_pi_system.insert_univ {α : Type u_1} {S : set (set α)} (h_pi : is_pi_system S) :

is_pi_system (has_insert.insert set.univ S)

source

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}

source

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)

source

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)

source

theorem is_pi_system_image_Iio {α : Type u_1} [linear_order α] (s : set α) :

is_pi_system (set.Iio '' s)

source

theorem is_pi_system_Iio {α : Type u_1} [linear_order α] :

is_pi_system (set.range set.Iio)

source

theorem is_pi_system_image_Ioi {α : Type u_1} [linear_order α] (s : set α) :

is_pi_system (set.Ioi '' s)

source

theorem is_pi_system_Ioi {α : Type u_1} [linear_order α] :

is_pi_system (set.range set.Ioi)

source

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}

source

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}

source

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}

source

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}

source

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}

source

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}

source

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}

source

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}

source

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}

source

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}

source

inductive generate_pi_system {α : Type u_1} (S : set (set α)) :

set (set α)

base : ∀ {α : Type u_1} {S : set (set α)} {s : set α}, s ∈ S → generate_pi_system S s
inter : ∀ {α : Type u_1} {S : set (set α)} {s t : set α}, generate_pi_system S s → generate_pi_system S t → (s ∩ t).nonempty → generate_pi_system S (s ∩ t)

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

source

theorem is_pi_system_generate_pi_system {α : Type u_1} (S : set (set α)) :

is_pi_system (generate_pi_system S)

source

theorem subset_generate_pi_system_self {α : Type u_1} (S : set (set α)) :

S ⊆ generate_pi_system S

source

theorem generate_pi_system_subset_self {α : Type u_1} {S : set (set α)} (h_S : is_pi_system S) :

generate_pi_system S ⊆ S

source

theorem generate_pi_system_eq {α : Type u_1} {S : set (set α)} (h_pi : is_pi_system S) :

generate_pi_system S = S

source

theorem generate_pi_system_mono {α : Type u_1} {S T : set (set α)} (hST : S ⊆ T) :

generate_pi_system S ⊆ generate_pi_system T

source

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) :

measurable_set t

source

theorem generate_from_measurable_set_of_generate_pi_system {α : Type u_1} {g : set (set α)} (t : set α) (ht : t ∈ generate_pi_system g) :

measurable_set t

source

theorem generate_from_generate_pi_system_eq {α : Type u_1} {g : set (set α)} :

measurable_space.generate_from (generate_pi_system g) = measurable_space.generate_from g

source

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

source

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 #

source

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

pi_Union_Inter π S = {s : set α | ∃ (t : finset ι) (htS : ↑t ⊆ S) (f : ι → set α) (hf : ∀ (x : ι), x ∈ t → f x ∈ π x), s = ⋂ (x : ι) (H : x ∈ t), f x}

source

theorem pi_Union_Inter_singleton {α : Type u_1} {ι : Type u_2} (π : ι → set (set α)) (i : ι) :

pi_Union_Inter π {i} = π i ∪ {set.univ}

source

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}

source

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}

source

theorem is_pi_system_pi_Union_Inter {α : Type u_1} {ι : Type u_2} (π : ι → set (set α)) (hpi : ∀ (x : ι), is_pi_system (π x)) (S : set ι) :

is_pi_system (pi_Union_Inter π S)

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

source

theorem pi_Union_Inter_mono_left {α : Type u_1} {ι : Type u_2} {π π' : ι → set (set α)} (h_le : ∀ (i : ι), π i ⊆ π' i) (S : set ι) :

pi_Union_Inter π S ⊆ pi_Union_Inter π' S

source

theorem pi_Union_Inter_mono_right {α : Type u_1} {ι : Type u_2} {π : ι → set (set α)} {S T : set ι} (hST : S ⊆ T) :

pi_Union_Inter π S ⊆ pi_Union_Inter π T

source

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 ι) :

measurable_space.generate_from (pi_Union_Inter π S) ≤ m

source

theorem subset_pi_Union_Inter {α : Type u_1} {ι : Type u_2} {π : ι → set (set α)} {S : set ι} {i : ι} (his : i ∈ S) :

π i ⊆ pi_Union_Inter π S

source

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

source

theorem le_generate_from_pi_Union_Inter {α : Type u_1} {ι : Type u_2} {π : ι → set (set α)} (S : set ι) {x : ι} (hxS : x ∈ S) :

measurable_space.generate_from (π x) ≤ measurable_space.generate_from (pi_Union_Inter π S)

source

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) :

measurable_set t

source

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 #

source

structure measurable_space.dynkin_system (α : Type u_2) :

Type u_2

has : set α → Prop
has_empty : self.has ∅
has_compl : ∀ {a : set α}, self.has a → self.has aᶜ
has_Union_nat : ∀ {f : ℕ → set α}, pairwise (disjoint on f) → (∀ (i : ℕ), self.has (f i)) → self.has (⋃ (i : ℕ), f i)

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

measurable_space.dynkin_system.has_sizeof_inst
measurable_space.dynkin_system.has_le
measurable_space.dynkin_system.partial_order
measurable_space.dynkin_system.inhabited

source

@[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₂

source

theorem measurable_space.dynkin_system.has_compl_iff {α : Type u_1} (d : measurable_space.dynkin_system α) {a : set α} :

d.has aᶜ ↔ d.has a

source

theorem measurable_space.dynkin_system.has_univ {α : Type u_1} (d : measurable_space.dynkin_system α) :

d.has set.univ

source

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)

source

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₂)

source

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₂)

source

@[protected, instance]

def measurable_space.dynkin_system.has_le {α : Type u_1} :

has_le (measurable_space.dynkin_system α)

Equations

measurable_space.dynkin_system.has_le = {le := λ (m₁ m₂ : measurable_space.dynkin_system α), m₁.has ≤ m₂.has}

source

theorem measurable_space.dynkin_system.le_def {α : Type u_1} {a b : measurable_space.dynkin_system α} :

a ≤ b ↔ a.has ≤ b.has

source

@[protected, instance]

def measurable_space.dynkin_system.partial_order {α : Type u_1} :

partial_order (measurable_space.dynkin_system α)

Equations

measurable_space.dynkin_system.partial_order = {le := has_le.le measurable_space.dynkin_system.has_le, lt := preorder.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

def measurable_space.dynkin_system.of_measurable_space {α : Type u_1} (m : measurable_space α) :

measurable_space.dynkin_system α

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

Equations

measurable_space.dynkin_system.of_measurable_space m = {has := m.measurable_set', has_empty := _, has_compl := _, has_Union_nat := _}

source

theorem measurable_space.dynkin_system.of_measurable_space_le_of_measurable_space_iff {α : Type u_1} {m₁ m₂ : measurable_space α} :

measurable_space.dynkin_system.of_measurable_space m₁ ≤ measurable_space.dynkin_system.of_measurable_space m₂ ↔ m₁ ≤ m₂

source

inductive measurable_space.dynkin_system.generate_has {α : Type u_1} (s : set (set α)) :

set α → Prop

basic : ∀ {α : Type u_1} {s : set (set α)} (t : set α), t ∈ s → measurable_space.dynkin_system.generate_has s t
empty : ∀ {α : Type u_1} {s : set (set α)}, measurable_space.dynkin_system.generate_has s ∅
compl : ∀ {α : Type u_1} {s : set (set α)} {a : set α}, measurable_space.dynkin_system.generate_has s a → measurable_space.dynkin_system.generate_has s aᶜ
Union : ∀ {α : Type u_1} {s : set (set α)} {f : ℕ → set α}, pairwise (disjoint on f) → (∀ (i : ℕ), measurable_space.dynkin_system.generate_has s (f i)) → measurable_space.dynkin_system.generate_has s (⋃ (i : ℕ), f i)

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

source

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

measurable_space.dynkin_system.generate_has C sᶜ ↔ measurable_space.dynkin_system.generate_has C s

source

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

measurable_space.dynkin_system α

The least Dynkin system containing a collection of basic sets.

Equations

measurable_space.dynkin_system.generate s = {has := measurable_space.dynkin_system.generate_has s, has_empty := _, has_compl := _, has_Union_nat := _}

source

theorem measurable_space.dynkin_system.generate_has_def {α : Type u_1} {C : set (set α)} :

(measurable_space.dynkin_system.generate C).has = measurable_space.dynkin_system.generate_has C

source

@[protected, instance]

def measurable_space.dynkin_system.inhabited {α : Type u_1} :

inhabited (measurable_space.dynkin_system α)

Equations

measurable_space.dynkin_system.inhabited = {default := measurable_space.dynkin_system.generate set.univ}

source

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₂)) :

measurable_space α

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

Equations

d.to_measurable_space h_inter = {measurable_set' := d.has, measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}

source

theorem measurable_space.dynkin_system.of_measurable_space_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₂)) :

measurable_space.dynkin_system.of_measurable_space (d.to_measurable_space h_inter) = d

source

def measurable_space.dynkin_system.restrict_on {α : Type u_1} (d : measurable_space.dynkin_system α) {s : set α} (h : d.has s) :

measurable_space.dynkin_system α

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

Equations

d.restrict_on h = {has := λ (t : set α), d.has (t ∩ s), has_empty := _, has_compl := _, has_Union_nat := _}

source

theorem measurable_space.dynkin_system.generate_le {α : Type u_1} (d : measurable_space.dynkin_system α) {s : set (set α)} (h : ∀ (t : set α), t ∈ s → d.has t) :

measurable_space.dynkin_system.generate s ≤ d

source

theorem measurable_space.dynkin_system.generate_has_subset_generate_measurable {α : Type u_1} {C : set (set α)} {s : set α} (hs : (measurable_space.dynkin_system.generate C).has s) :

measurable_set s

source

theorem measurable_space.dynkin_system.generate_inter {α : Type u_1} {s : set (set α)} (hs : is_pi_system s) {t₁ t₂ : set α} (ht₁ : (measurable_space.dynkin_system.generate s).has t₁) (ht₂ : (measurable_space.dynkin_system.generate s).has t₂) :

(measurable_space.dynkin_system.generate s).has (t₁ ∩ t₂)

source

theorem measurable_space.dynkin_system.generate_from_eq {α : Type u_1} {s : set (set α)} (hs : is_pi_system s) :

measurable_space.generate_from s = (measurable_space.dynkin_system.generate s).to_measurable_space _

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

source

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 α⦄ :

measurable_set t → C t

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

Main statements #

Implementation details #

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

Dynkin systems and Π-λ theorem #