mathlibdocumentation

probability_theory.independence

Independence of sets of sets and measure spaces (σ-algebras) #

• A family of sets of sets π : ι → set (set α) is independent with respect to a measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ π i_1, ..., f i_n ∈ π i_n, μ (⋂ i in s, f i) = ∏ i in s, μ (f i). It will be used for families of π-systems.
• A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a measure μ (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. I.e., m : ι → measurable_space α is independent with respect to a measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ m i_1, ..., f i_n ∈ m i_n, then μ (⋂ i in s, f i) = ∏ i in s, μ (f i).
• Independence of sets (or events in probabilistic parlance) is defined as independence of the measurable space structures they generate: a set s generates the measurable space structure with measurable sets ∅, s, sᶜ, univ.
• Independence of functions (or random variables) is also defined as independence of the measurable space structures they generate: a function f for which we have a measurable space m on the codomain generates measurable_space.comap f m.

Main statements #

• TODO: Indep_of_Indep_sets: if π-systems are independent as sets of sets, then the measurable space structures they generate are independent.
• indep_of_indep_sets: variant with two π-systems.

Implementation notes #

We provide one main definition of independence:

• Indep_sets: independence of a family of sets of sets pi : ι → set (set α). Three other independence notions are defined using Indep_sets:
• Indep: independence of a family of measurable space structures m : ι → measurable_space α,
• Indep_set: independence of a family of sets s : ι → set α,
• Indep_fun: independence of a family of functions. For measurable spaces m : Π (i : ι), measurable_space (β i), we consider functions f : Π (i : ι), α → β i.

Additionally, we provide four corresponding statements for two measurable space structures (resp. sets of sets, sets, functions) instead of a family. These properties are denoted by the same names as for a family, but without a capital letter, for example indep_fun is the version of Indep_fun for two functions.

The definition of independence for Indep_sets uses finite sets (finset). An alternative and equivalent way of defining independence would have been to use countable sets. TODO: prove that equivalence.

Most of the definitions and lemma in this file list all variables instead of using the variables keyword at the beginning of a section, for example lemma indep.symm {α} {m₁ m₂ : measurable_space α} [measurable_space α] {μ : measure α} ... . This is intentional, to be able to control the order of the measurable_space variables. Indeed when defining μ in the example above, the measurable space used is the last one defined, here [measurable_space α], and not m₁ or m₂.

References #

• Williams, David. Probability with martingales. Cambridge university press, 1991. Part A, Chapter 4.
def probability_theory.Indep_sets {α : Type u_1} {ι : Type u_2} (π : ι → set (set α)) (μ : . "volume_tac") :
Prop

A family of sets of sets π : ι → set (set α) is independent with respect to a measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ π i_1, ..., f i_n ∈ π i_n, then μ (⋂ i in s, f i) = ∏ i in s, μ (f i). It will be used for families of pi_systems.

Equations
• = ∀ (s : finset ι) {f : ι → set α}, (∀ (i : ι), i sf i «π» i)μ (⋂ (i : ι) (H : i s), f i) = ∏ (i : ι) in s, μ (f i)
def probability_theory.indep_sets {α : Type u_1} (s1 s2 : set (set α)) (μ : . "volume_tac") :
Prop

Two sets of sets s₁, s₂ are independent with respect to a measure μ if for any sets t₁ ∈ p₁, t₂ ∈ s₂, then μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)

Equations
def probability_theory.Indep {α : Type u_1} {ι : Type u_2} (m : ι → ) (μ : . "volume_tac") :
Prop

A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a measure μ (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. m : ι → measurable_space α is independent with respect to measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ m i_1, ..., f i_n ∈ m i_n, then μ (⋂ i in s, f i) = ∏ i in s, μ (f i).

Equations
def probability_theory.indep {α : Type u_1} (m₁ m₂ : measurable_space α) (μ : . "volume_tac") :
Prop

Two measurable space structures (or σ-algebras) m₁, m₂ are independent with respect to a measure μ (defined on a third σ-algebra) if for any sets t₁ ∈ m₁, t₂ ∈ m₂, μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)

Equations
def probability_theory.Indep_set {α : Type u_1} {ι : Type u_2} (s : ι → set α) (μ : . "volume_tac") :
Prop

A family of sets is independent if the family of measurable space structures they generate is independent. For a set s, the generated measurable space has measurable sets ∅, s, sᶜ, univ.

Equations
def probability_theory.indep_set {α : Type u_1} (s t : set α) (μ : . "volume_tac") :
Prop

Two sets are independent if the two measurable space structures they generate are independent. For a set s, the generated measurable space structure has measurable sets ∅, s, sᶜ, univ.

Equations
def probability_theory.Indep_fun {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} (m : Π (x : ι), measurable_space (β x)) (f : Π (x : ι), α → β x) (μ : . "volume_tac") :
Prop

A family of functions defined on the same space α and taking values in possibly different spaces, each with a measurable space structure, is independent if the family of measurable space structures they generate on α is independent. For a function g with codomain having measurable space structure m, the generated measurable space structure is measurable_space.comap g m.

Equations
def probability_theory.indep_fun {α : Type u_1} {β : Type u_2} {γ : Type u_3} (mβ : measurable_space β) (mγ : measurable_space γ) (f : α → β) (g : α → γ) (μ : . "volume_tac") :
Prop

Two functions are independent if the two measurable space structures they generate are independent. For a function f with codomain having measurable space structure m, the generated measurable space structure is measurable_space.comap f m.

Equations
• f g μ = μ
theorem probability_theory.indep_sets.symm {α : Type u_1} {s₁ s₂ : set (set α)} {μ : measure_theory.measure α} (h : μ) :
theorem probability_theory.indep.symm {α : Type u_1} {m₁ m₂ : measurable_space α} {μ : measure_theory.measure α} (h : μ) :
μ
theorem probability_theory.indep_sets_of_indep_sets_of_le_left {α : Type u_1} {s₁ s₂ s₃ : set (set α)} {μ : measure_theory.measure α} (h_indep : μ) (h31 : s₃ s₁) :
theorem probability_theory.indep_sets_of_indep_sets_of_le_right {α : Type u_1} {s₁ s₂ s₃ : set (set α)} {μ : measure_theory.measure α} (h_indep : μ) (h32 : s₃ s₂) :
theorem probability_theory.indep_of_indep_of_le_left {α : Type u_1} {m₁ m₂ m₃ : measurable_space α} {μ : measure_theory.measure α} (h_indep : μ) (h31 : m₃ m₁) :
μ
theorem probability_theory.indep_of_indep_of_le_right {α : Type u_1} {m₁ m₂ m₃ : measurable_space α} {μ : measure_theory.measure α} (h_indep : μ) (h32 : m₃ m₂) :
μ
theorem probability_theory.indep_sets.union {α : Type u_1} {s₁ s₂ s' : set (set α)} {μ : measure_theory.measure α} (h₁ : μ) (h₂ : μ) :
@[simp]
theorem probability_theory.indep_sets.union_iff {α : Type u_1} {s₁ s₂ s' : set (set α)} {μ : measure_theory.measure α} :
theorem probability_theory.indep_sets.Union {α : Type u_1} {ι : Sort u_2} {s : ι → set (set α)} {s' : set (set α)} {μ : measure_theory.measure α} (hyp : ∀ (n : ι), s' μ) :
probability_theory.indep_sets (⋃ (n : ι), s n) s' μ
theorem probability_theory.indep_sets.inter {α : Type u_1} {s₁ s' : set (set α)} (s₂ : set (set α)) {μ : measure_theory.measure α} (h₁ : μ) :
theorem probability_theory.indep_sets.Inter {α : Type u_1} {ι : Sort u_2} {s : ι → set (set α)} {s' : set (set α)} {μ : measure_theory.measure α} (h : ∃ (n : ι), s' μ) :
probability_theory.indep_sets (⋂ (n : ι), s n) s' μ

Deducing indep from Indep#

theorem probability_theory.Indep_sets.indep_sets {α : Type u_1} {ι : Type u_2} {s : ι → set (set α)} {μ : measure_theory.measure α} (h_indep : μ) {i j : ι} (hij : i j) :
(s j) μ
theorem probability_theory.Indep.indep {α : Type u_1} {ι : Type u_2} {m : ι → } {μ : measure_theory.measure α} (h_indep : μ) {i j : ι} (hij : i j) :
(m j) μ

π-system lemma #

Independence of measurable spaces is equivalent to independence of generating π-systems.

Independence of measurable space structures implies independence of generating π-systems #

theorem probability_theory.Indep.Indep_sets {α : Type u_1} {ι : Type u_2} {μ : measure_theory.measure α} {m : ι → } {s : ι → set (set α)} (hms : ∀ (n : ι), m n = ) (h_indep : μ) :
theorem probability_theory.indep.indep_sets {α : Type u_1} {μ : measure_theory.measure α} {s1 s2 : set (set α)} (h_indep : μ) :

Independence of generating π-systems implies independence of measurable space structures #

theorem probability_theory.indep_sets.indep {α : Type u_1} {m1 m2 m : measurable_space α} {μ : measure_theory.measure α} {p1 p2 : set (set α)} (h1 : m1 m) (h2 : m2 m) (hp1 : is_pi_system p1) (hp2 : is_pi_system p2) (hpm1 : m1 = ) (hpm2 : m2 = ) (hyp : μ) :
μ