# mathlibdocumentation

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

• Indep_sets.Indep: if π-systems are independent as sets of sets, then the measurable space structures they generate are independent.
• indep_sets.indep: variant with two π-systems.
• measure_zero_or_one_of_measurable_set_limsup_at_top: Kolmogorov's 0-1 law. Any set which is measurable with respect to the tail σ-algebra limsup s at_top of an independent sequence of σ-algebras s has probability 0 or 1.

## 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
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
@[symm]
theorem probability_theory.indep_sets.symm {Ω : Type u_1} {s₁ s₂ : set (set Ω)} {μ : measure_theory.measure Ω} (h : μ) :
@[symm]
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} {ι : Type 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.bUnion {Ω : Type u_1} {ι : Type u_2} {s : ι set (set Ω)} {s' : set (set Ω)} {μ : measure_theory.measure Ω} {u : set ι} (hyp : (n : ι), n u s' μ) :
probability_theory.indep_sets ( (n : ι) (H : n u), 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} {ι : Type u_2} {s : ι set (set Ω)} {s' : set (set Ω)} {μ : measure_theory.measure Ω} (h : (n : ι), s' μ) :
probability_theory.indep_sets ( (n : ι), s n) s' μ
theorem probability_theory.indep_sets.bInter {Ω : Type u_1} {ι : Type u_2} {s : ι set (set Ω)} {s' : set (set Ω)} {μ : measure_theory.measure Ω} {u : set ι} (h : (n : ι) (H : n u), s' μ) :
probability_theory.indep_sets ( (n : ι) (H : n u), s n) s' μ
theorem probability_theory.indep_sets_singleton_iff {Ω : Type u_1} {s t : set Ω} {μ : measure_theory.measure Ω} :
μ μ (s t) = μ s * μ t

### 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) μ
theorem probability_theory.Indep_fun.indep_fun {Ω : Type u_1} {ι : Type u_2} {m₀ : measurable_space Ω} {μ : measure_theory.measure Ω} {β : ι Type u_3} {m : Π (x : ι), measurable_space (β x)} {f : Π (i : ι), Ω β i} (hf_Indep : μ) {i j : ι} (hij : i j) :
(f 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 : μ) :
μ
theorem probability_theory.indep_sets.indep' {Ω : Type u_1} {m : measurable_space Ω} {μ : measure_theory.measure Ω} {p1 p2 : set (set Ω)} (hp1m : (s : set Ω), s p1 ) (hp2m : (s : set Ω), s p2 ) (hp1 : is_pi_system p1) (hp2 : is_pi_system p2) (hyp : μ) :
theorem probability_theory.indep_sets_pi_Union_Inter_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι set (set Ω)} {S T : set ι} (h_indep : μ) (hST : T) :
μ
theorem probability_theory.Indep_set.indep_generate_from_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι set Ω} (hsm : (n : ι), measurable_set (s n)) (hs : μ) (S T : set ι) (hST : T) :
probability_theory.indep (measurable_space.generate_from {t : set Ω | (n : ι) (H : n S), s n = t}) (measurable_space.generate_from {t : set Ω | (k : ι) (H : k T), s k = t}) μ
theorem probability_theory.indep_supr_of_disjoint {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {m : ι } (h_le : (i : ι), m i m0) (h_indep : μ) {S T : set ι} (hST : T) :
probability_theory.indep ( (i : ι) (H : i S), m i) ( (i : ι) (H : i T), m i) μ
theorem probability_theory.indep_supr_of_directed_le {ι : Type u_2} {Ω : Type u_1} {m : ι } {m' m0 : measurable_space Ω} {μ : measure_theory.measure Ω} (h_indep : (i : ι), m' μ) (h_le : (i : ι), m i m0) (h_le' : m' m0) (hm : m) :
probability_theory.indep ( (i : ι), m i) m' μ
theorem probability_theory.Indep_set.indep_generate_from_lt {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [preorder ι] {s : ι set Ω} (hsm : (n : ι), measurable_set (s n)) (hs : μ) (i : ι) :
(measurable_space.generate_from {t : set Ω | (j : ι) (H : j < i), s j = t}) μ
theorem probability_theory.Indep_set.indep_generate_from_le {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [linear_order ι] {s : ι set Ω} (hsm : (n : ι), measurable_set (s n)) (hs : μ) (i : ι) {k : ι} (hk : i < k) :
(measurable_space.generate_from {t : set Ω | (j : ι) (H : j i), s j = t}) μ
theorem probability_theory.Indep_set.indep_generate_from_le_nat {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : set Ω} (hsm : (n : ), measurable_set (s n)) (hs : μ) (n : ) :
(measurable_space.generate_from {t : set Ω | (k : ) (H : k n), s k = t}) μ
theorem probability_theory.indep_supr_of_monotone {ι : Type u_2} {Ω : Type u_1} {m : ι } {m' m0 : measurable_space Ω} {μ : measure_theory.measure Ω} (h_indep : (i : ι), m' μ) (h_le : (i : ι), m i m0) (h_le' : m' m0) (hm : monotone m) :
probability_theory.indep ( (i : ι), m i) m' μ
theorem probability_theory.indep_supr_of_antitone {ι : Type u_2} {Ω : Type u_1} {m : ι } {m' m0 : measurable_space Ω} {μ : measure_theory.measure Ω} (h_indep : (i : ι), m' μ) (h_le : (i : ι), m i m0) (h_le' : m' m0) (hm : antitone m) :
probability_theory.indep ( (i : ι), m i) m' μ
theorem probability_theory.Indep_sets.pi_Union_Inter_of_not_mem {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {π : ι set (set Ω)} {a : ι} {S : finset ι} (hp_ind : μ) (haS : a S) :
(π a) μ
theorem probability_theory.Indep_sets.Indep {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} (m : ι ) (h_le : (i : ι), m i m0) (π : ι set (set Ω)) (h_pi : (n : ι), is_pi_system (π n)) (h_generate : (i : ι), m i = ) (h_ind : μ) :

The measurable space structures generated by independent pi-systems are independent.

### Independence of measurable sets #

We prove the following equivalences on indep_set, for measurable sets s, t.

• indep_set s t μ ↔ μ (s ∩ t) = μ s * μ t,
• indep_set s t μ ↔ indep_sets {s} {t} μ.
theorem probability_theory.indep_set_iff_indep_sets_singleton {Ω : Type u_1} {s t : set Ω} {m0 : measurable_space Ω} (hs_meas : measurable_set s) (ht_meas : measurable_set t) (μ : . "volume_tac")  :
μ
theorem probability_theory.indep_set_iff_measure_inter_eq_mul {Ω : Type u_1} {s t : set Ω} {m0 : measurable_space Ω} (hs_meas : measurable_set s) (ht_meas : measurable_set t) (μ : . "volume_tac")  :
μ (s t) = μ s * μ t
theorem probability_theory.indep_sets.indep_set_of_mem {Ω : Type u_1} {s t : set Ω} (S T : set (set Ω)) {m0 : measurable_space Ω} (hs : s S) (ht : t T) (hs_meas : measurable_set s) (ht_meas : measurable_set t) (μ : . "volume_tac") (h_indep : μ) :
theorem probability_theory.indep.indep_set_of_measurable_set {Ω : Type u_1} {m₁ m₂ m0 : measurable_space Ω} {μ : measure_theory.measure Ω} (h_indep : μ) {s t : set Ω} (hs : measurable_set s) (ht : measurable_set t) :
theorem probability_theory.indep_iff_forall_indep_set {Ω : Type u_1} (m₁ m₂ : measurable_space Ω) {m0 : measurable_space Ω} (μ : measure_theory.measure Ω) :
μ (s t : set Ω),

### Independence of random variables #

theorem probability_theory.indep_fun_iff_measure_inter_preimage_eq_mul {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω β} {g : Ω β'} {mβ : measurable_space β} {mβ' : measurable_space β'} :
(s : set β) (t : set β'), μ (f ⁻¹' s g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)
theorem probability_theory.Indep_fun_iff_measure_inter_preimage_eq_mul {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : ι Type u_3} (m : Π (x : ι), measurable_space (β x)) (f : Π (i : ι), Ω β i) :
(S : finset ι) {sets : Π (i : ι), set (β i)}, ( (i : ι), i S measurable_set (sets i)) μ ( (i : ι) (H : i S), f i ⁻¹' sets i) = S.prod (λ (i : ι), μ (f i ⁻¹' sets i))
theorem probability_theory.indep_fun_iff_indep_set_preimage {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω β} {g : Ω β'} {mβ : measurable_space β} {mβ' : measurable_space β'} (hf : measurable f) (hg : measurable g) :
(s : set β) (t : set β'), (g ⁻¹' t) μ
@[symm]
theorem probability_theory.indep_fun.symm {Ω : Type u_1} {β : Type u_3} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {mβ : measurable_space β} {f g : Ω β} (hfg : μ) :
theorem probability_theory.indep_fun.ae_eq {Ω : Type u_1} {β : Type u_3} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {mβ : measurable_space β} {f g f' g' : Ω β} (hfg : μ) (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') :
μ
theorem probability_theory.indep_fun.comp {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {γ' : Type u_6} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {f : Ω β} {g : Ω β'} {mβ : measurable_space β} {mβ' : measurable_space β'} {mγ : measurable_space γ} {mγ' : measurable_space γ'} {φ : β γ} {ψ : β' γ'} (hfg : μ) (hφ : measurable φ) (hψ : measurable ψ) :
g) μ
theorem probability_theory.Indep_fun.indep_fun_finset {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : ι Type u_3} {m : Π (i : ι), measurable_space (β i)} {f : Π (i : ι), Ω β i} (S T : finset ι) (hST : T) (hf_Indep : μ) (hf_meas : (i : ι), measurable (f i)) :
probability_theory.indep_fun (λ (a : Ω) (i : S), f i a) (λ (a : Ω) (i : T), f i a) μ

If f is a family of mutually independent random variables (Indep_fun m f μ) and S, T are two disjoint finite index sets, then the tuple formed by f i for i ∈ S is independent of the tuple (f i)_i for i ∈ T.

theorem probability_theory.Indep_fun.indep_fun_prod {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : ι Type u_3} {m : Π (i : ι), measurable_space (β i)} {f : Π (i : ι), Ω β i} (hf_Indep : μ) (hf_meas : (i : ι), measurable (f i)) (i j k : ι) (hik : i k) (hjk : j k) :
probability_theory.indep_fun (λ (a : Ω), (f i a, f j a)) (f k) μ
theorem probability_theory.Indep_fun.mul {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : Type u_3} {m : measurable_space β} [has_mul β] {f : ι Ω β} (hf_Indep : probability_theory.Indep_fun (λ (_x : ι), m) f μ) (hf_meas : (i : ι), measurable (f i)) (i j k : ι) (hik : i k) (hjk : j k) :
probability_theory.indep_fun (f i * f j) (f k) μ
theorem probability_theory.Indep_fun.add {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : Type u_3} {m : measurable_space β} [has_add β] {f : ι Ω β} (hf_Indep : probability_theory.Indep_fun (λ (_x : ι), m) f μ) (hf_meas : (i : ι), measurable (f i)) (i j k : ι) (hik : i k) (hjk : j k) :
probability_theory.indep_fun (f i + f j) (f k) μ
theorem probability_theory.Indep_fun.indep_fun_finset_sum_of_not_mem {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : Type u_3} {m : measurable_space β} {f : ι Ω β} (hf_Indep : probability_theory.Indep_fun (λ (_x : ι), m) f μ) (hf_meas : (i : ι), measurable (f i)) {s : finset ι} {i : ι} (hi : i s) :
probability_theory.indep_fun (s.sum (λ (j : ι), f j)) (f i) μ
theorem probability_theory.Indep_fun.indep_fun_finset_prod_of_not_mem {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {ι : Type u_2} {β : Type u_3} {m : measurable_space β} [comm_monoid β] {f : ι Ω β} (hf_Indep : probability_theory.Indep_fun (λ (_x : ι), m) f μ) (hf_meas : (i : ι), measurable (f i)) {s : finset ι} {i : ι} (hi : i s) :
probability_theory.indep_fun (s.prod (λ (j : ι), f j)) (f i) μ
theorem probability_theory.Indep_fun.indep_fun_prod_range_succ {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {β : Type u_2} {m : measurable_space β} [comm_monoid β] {f : Ω β} (hf_Indep : probability_theory.Indep_fun (λ (_x : ), m) f μ) (hf_meas : (i : ), measurable (f i)) (n : ) :
probability_theory.indep_fun ((finset.range n).prod (λ (j : ), f j)) (f n) μ
theorem probability_theory.Indep_fun.indep_fun_sum_range_succ {Ω : Type u_1} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} {β : Type u_2} {m : measurable_space β} {f : Ω β} (hf_Indep : probability_theory.Indep_fun (λ (_x : ), m) f μ) (hf_meas : (i : ), measurable (f i)) (n : ) :
probability_theory.indep_fun ((finset.range n).sum (λ (j : ), f j)) (f n) μ
theorem probability_theory.Indep_set.Indep_fun_indicator {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {mΩ : measurable_space Ω} {μ : measure_theory.measure Ω} [has_zero β] [has_one β] {m : measurable_space β} {s : ι set Ω} (hs : μ) :
probability_theory.Indep_fun (λ (n : ι), m) (λ (n : ι), (s n).indicator (λ (ω : Ω), 1)) μ

### Kolmogorov's 0-1 law #

Let s : ι → measurable_space Ω be an independent sequence of sub-σ-algebras. Then any set which is measurable with respect to the tail σ-algebra limsup s at_top has probability 0 or 1.

theorem probability_theory.measure_eq_zero_or_one_or_top_of_indep_set_self {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {t : set Ω} (h_indep : μ) :
μ t = 0 μ t = 1 μ t =
theorem probability_theory.measure_eq_zero_or_one_of_indep_set_self {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {t : set Ω} (h_indep : μ) :
μ t = 0 μ t = 1
theorem probability_theory.indep_bsupr_compl {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } (h_le : (n : ι), s n m0) (h_indep : μ) (t : set ι) :
probability_theory.indep ( (n : ι) (H : n t), s n) ( (n : ι) (H : n t), s n) μ

We prove a version of Kolmogorov's 0-1 law for the σ-algebra limsup s f where f is a filter for which we can define the following two functions:

• p : set ι → Prop such that for a set t, p t → tᶜ ∈ f,
• ns : α → set ι a directed sequence of sets which all verify p and such that ⋃ a, ns a = set.univ.

For the example of f = at_top, we can take p = bdd_above and ns : ι → set ι := λ i, set.Iic i.

theorem probability_theory.indep_bsupr_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {p : set ι Prop} {f : filter ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) {t : set ι} (ht : p t) :
probability_theory.indep ( (n : ι) (H : n t), s n) f) μ
theorem probability_theory.indep_supr_directed_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {α : Type u_3} {p : set ι Prop} {f : filter ι} {ns : α set ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) (hns : ns) (hnsp : (a : α), p (ns a)) :
probability_theory.indep ( (a : α) (n : ι) (H : n ns a), s n) f) μ
theorem probability_theory.indep_supr_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {α : Type u_3} {p : set ι Prop} {f : filter ι} {ns : α set ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) (hns : ns) (hnsp : (a : α), p (ns a)) (hns_univ : (n : ι), (a : α), n ns a) :
probability_theory.indep ( (n : ι), s n) f) μ
theorem probability_theory.indep_limsup_self {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {α : Type u_3} {p : set ι Prop} {f : filter ι} {ns : α set ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) (hns : ns) (hnsp : (a : α), p (ns a)) (hns_univ : (n : ι), (a : α), n ns a) :
f) μ
theorem probability_theory.measure_zero_or_one_of_measurable_set_limsup {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } {α : Type u_3} {p : set ι Prop} {f : filter ι} {ns : α set ι} (h_le : (n : ι), s n m0) (h_indep : μ) (hf : (t : set ι), p t t f) (hns : ns) (hnsp : (a : α), p (ns a)) (hns_univ : (n : ι), (a : α), n ns a) {t : set Ω} (ht_tail : measurable_set t) :
μ t = 0 μ t = 1
theorem probability_theory.indep_limsup_at_top_self {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } [no_max_order ι] [nonempty ι] (h_le : (n : ι), s n m0) (h_indep : μ) :
theorem probability_theory.measure_zero_or_one_of_measurable_set_limsup_at_top {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } [no_max_order ι] [nonempty ι] (h_le : (n : ι), s n m0) (h_indep : μ) {t : set Ω} (ht_tail : measurable_set t) :
μ t = 0 μ t = 1

Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1. The tail σ-algebra limsup s at_top is the same as ⋂ n, ⋃ i ≥ n, s i.

theorem probability_theory.indep_limsup_at_bot_self {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } [no_min_order ι] [nonempty ι] (h_le : (n : ι), s n m0) (h_indep : μ) :
theorem probability_theory.measure_zero_or_one_of_measurable_set_limsup_at_bot {Ω : Type u_1} {ι : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {s : ι } [no_min_order ι] [nonempty ι] (h_le : (n : ι), s n m0) (h_indep : μ) {t : set Ω} (ht_tail : measurable_set t) :
μ t = 0 μ t = 1

Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1.