Independence of sets of sets and measure spaces (σ-algebras) #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
- A family of sets of sets
π : ι → set (set Ω)is independent with respect to a measureμif for any finite set of indicess = {i_1, ..., i_n}, for any setsf 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 indicess = {i_1, ..., i_n}, for any setsf 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
sgenerates 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
ffor which we have a measurable spacemon the codomain generatesmeasurable_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.
Implementation notes #
We provide one main definition of independence:
Indep_sets: independence of a family of sets of setspi : ι → set (set Ω). Three other independence notions are defined usingIndep_sets:Indep: independence of a family of measurable space structuresm : ι → measurable_space Ω,Indep_set: independence of a family of setss : ι → set Ω,Indep_fun: independence of a family of functions. For measurable spacesm : Π (i : ι), measurable_space (β i), we consider functionsf : Π (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}
[measurable_space Ω]
(π : ι → set (set Ω))
(μ : measure_theory.measure Ω . "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.
def
probability_theory.indep_sets
{Ω : Type u_1}
[measurable_space Ω]
(s1 s2 : set (set Ω))
(μ : measure_theory.measure Ω . "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₂)
def
probability_theory.Indep
{Ω : Type u_1}
{ι : Type u_2}
(m : ι → measurable_space Ω)
[measurable_space Ω]
(μ : measure_theory.measure Ω . "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
- probability_theory.Indep m μ = probability_theory.Indep_sets (λ (x : ι), {s : set Ω | measurable_set s}) μ
def
probability_theory.indep
{Ω : Type u_1}
(m₁ m₂ : measurable_space Ω)
[measurable_space Ω]
(μ : measure_theory.measure Ω . "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
- probability_theory.indep m₁ m₂ μ = probability_theory.indep_sets {s : set Ω | measurable_set s} {s : set Ω | measurable_set s} μ
def
probability_theory.Indep_set
{Ω : Type u_1}
{ι : Type u_2}
[measurable_space Ω]
(s : ι → set Ω)
(μ : measure_theory.measure Ω . "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
- probability_theory.Indep_set s μ = probability_theory.Indep (λ (i : ι), measurable_space.generate_from {s i}) μ
def
probability_theory.indep_set
{Ω : Type u_1}
[measurable_space Ω]
(s t : set Ω)
(μ : measure_theory.measure Ω . "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}
[measurable_space Ω]
{β : ι → Type u_3}
(m : Π (x : ι), measurable_space (β x))
(f : Π (x : ι), Ω → β x)
(μ : measure_theory.measure Ω . "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
- probability_theory.Indep_fun m f μ = probability_theory.Indep (λ (x : ι), measurable_space.comap (f x) (m x)) μ
def
probability_theory.indep_fun
{Ω : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space Ω]
[mβ : measurable_space β]
[mγ : measurable_space γ]
(f : Ω → β)
(g : Ω → γ)
(μ : measure_theory.measure Ω . "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
- probability_theory.indep_fun f g μ = probability_theory.indep (measurable_space.comap f mβ) (measurable_space.comap g mγ) μ
@[symm]
theorem
probability_theory.indep_sets.symm
{Ω : Type u_1}
{s₁ s₂ : set (set Ω)}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
(h : probability_theory.indep_sets s₁ s₂ μ) :
probability_theory.indep_sets s₂ s₁ μ
@[symm]
theorem
probability_theory.indep.symm
{Ω : Type u_1}
{m₁ m₂ : measurable_space Ω}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
(h : probability_theory.indep m₁ m₂ μ) :
probability_theory.indep m₂ m₁ μ
theorem
probability_theory.indep_bot_right
{Ω : Type u_1}
(m' : measurable_space Ω)
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ] :
theorem
probability_theory.indep_bot_left
{Ω : Type u_1}
(m' : measurable_space Ω)
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ] :
theorem
probability_theory.indep_set_empty_right
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(s : set Ω) :
theorem
probability_theory.indep_set_empty_left
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(s : set Ω) :
theorem
probability_theory.indep_sets_of_indep_sets_of_le_left
{Ω : Type u_1}
{s₁ s₂ s₃ : set (set Ω)}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
(h_indep : probability_theory.indep_sets s₁ s₂ μ)
(h31 : s₃ ⊆ s₁) :
probability_theory.indep_sets s₃ s₂ μ
theorem
probability_theory.indep_sets_of_indep_sets_of_le_right
{Ω : Type u_1}
{s₁ s₂ s₃ : set (set Ω)}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
(h_indep : probability_theory.indep_sets s₁ s₂ μ)
(h32 : s₃ ⊆ s₂) :
probability_theory.indep_sets s₁ s₃ μ
theorem
probability_theory.indep_of_indep_of_le_left
{Ω : Type u_1}
{m₁ m₂ m₃ : measurable_space Ω}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
(h_indep : probability_theory.indep m₁ m₂ μ)
(h31 : m₃ ≤ m₁) :
probability_theory.indep m₃ m₂ μ
theorem
probability_theory.indep_of_indep_of_le_right
{Ω : Type u_1}
{m₁ m₂ m₃ : measurable_space Ω}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
(h_indep : probability_theory.indep m₁ m₂ μ)
(h32 : m₃ ≤ m₂) :
probability_theory.indep m₁ m₃ μ
theorem
probability_theory.indep_sets.union
{Ω : Type u_1}
[measurable_space Ω]
{s₁ s₂ s' : set (set Ω)}
{μ : measure_theory.measure Ω}
(h₁ : probability_theory.indep_sets s₁ s' μ)
(h₂ : probability_theory.indep_sets s₂ s' μ) :
probability_theory.indep_sets (s₁ ∪ s₂) s' μ
@[simp]
theorem
probability_theory.indep_sets.union_iff
{Ω : Type u_1}
[measurable_space Ω]
{s₁ s₂ s' : set (set Ω)}
{μ : measure_theory.measure Ω} :
probability_theory.indep_sets (s₁ ∪ s₂) s' μ ↔ probability_theory.indep_sets s₁ s' μ ∧ probability_theory.indep_sets s₂ s' μ
theorem
probability_theory.indep_sets.Union
{Ω : Type u_1}
{ι : Type u_2}
[measurable_space Ω]
{s : ι → set (set Ω)}
{s' : set (set Ω)}
{μ : measure_theory.measure Ω}
(hyp : ∀ (n : ι), probability_theory.indep_sets (s n) s' μ) :
probability_theory.indep_sets (⋃ (n : ι), s n) s' μ
theorem
probability_theory.indep_sets.bUnion
{Ω : Type u_1}
{ι : Type u_2}
[measurable_space Ω]
{s : ι → set (set Ω)}
{s' : set (set Ω)}
{μ : measure_theory.measure Ω}
{u : set ι}
(hyp : ∀ (n : ι), n ∈ u → probability_theory.indep_sets (s n) s' μ) :
probability_theory.indep_sets (⋃ (n : ι) (H : n ∈ u), s n) s' μ
theorem
probability_theory.indep_sets.inter
{Ω : Type u_1}
[measurable_space Ω]
{s₁ s' : set (set Ω)}
(s₂ : set (set Ω))
{μ : measure_theory.measure Ω}
(h₁ : probability_theory.indep_sets s₁ s' μ) :
probability_theory.indep_sets (s₁ ∩ s₂) s' μ
theorem
probability_theory.indep_sets.Inter
{Ω : Type u_1}
{ι : Type u_2}
[measurable_space Ω]
{s : ι → set (set Ω)}
{s' : set (set Ω)}
{μ : measure_theory.measure Ω}
(h : ∃ (n : ι), probability_theory.indep_sets (s n) s' μ) :
probability_theory.indep_sets (⋂ (n : ι), s n) s' μ
theorem
probability_theory.indep_sets.bInter
{Ω : Type u_1}
{ι : Type u_2}
[measurable_space Ω]
{s : ι → set (set Ω)}
{s' : set (set Ω)}
{μ : measure_theory.measure Ω}
{u : set ι}
(h : ∃ (n : ι) (H : n ∈ u), probability_theory.indep_sets (s n) s' μ) :
probability_theory.indep_sets (⋂ (n : ι) (H : n ∈ u), s n) s' μ
theorem
probability_theory.indep_sets_singleton_iff
{Ω : Type u_1}
[measurable_space Ω]
{s t : set Ω}
{μ : measure_theory.measure Ω} :
Deducing indep from Indep #
theorem
probability_theory.Indep_sets.indep_sets
{Ω : Type u_1}
{ι : Type u_2}
{s : ι → set (set Ω)}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
(h_indep : probability_theory.Indep_sets s μ)
{i j : ι}
(hij : i ≠ j) :
probability_theory.indep_sets (s i) (s j) μ
theorem
probability_theory.Indep.indep
{Ω : Type u_1}
{ι : Type u_2}
{m : ι → measurable_space Ω}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
(h_indep : probability_theory.Indep m μ)
{i j : ι}
(hij : i ≠ j) :
probability_theory.indep (m i) (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 : probability_theory.Indep_fun m f μ)
{i j : ι}
(hij : i ≠ j) :
probability_theory.indep_fun (f i) (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}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
{m : ι → measurable_space Ω}
{s : ι → set (set Ω)}
(hms : ∀ (n : ι), m n = measurable_space.generate_from (s n))
(h_indep : probability_theory.Indep m μ) :
theorem
probability_theory.indep.indep_sets
{Ω : Type u_1}
[measurable_space Ω]
{μ : measure_theory.measure Ω}
{s1 s2 : set (set Ω)}
(h_indep : probability_theory.indep (measurable_space.generate_from s1) (measurable_space.generate_from s2) μ) :
probability_theory.indep_sets s1 s2 μ
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 Ω}
[measure_theory.is_probability_measure μ]
{p1 p2 : set (set Ω)}
(h1 : m1 ≤ m)
(h2 : m2 ≤ m)
(hp1 : is_pi_system p1)
(hp2 : is_pi_system p2)
(hpm1 : m1 = measurable_space.generate_from p1)
(hpm2 : m2 = measurable_space.generate_from p2)
(hyp : probability_theory.indep_sets p1 p2 μ) :
probability_theory.indep m1 m2 μ
theorem
probability_theory.indep_sets.indep'
{Ω : Type u_1}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{p1 p2 : set (set Ω)}
(hp1m : ∀ (s : set Ω), s ∈ p1 → measurable_set s)
(hp2m : ∀ (s : set Ω), s ∈ p2 → measurable_set s)
(hp1 : is_pi_system p1)
(hp2 : is_pi_system p2)
(hyp : probability_theory.indep_sets p1 p2 μ) :
theorem
probability_theory.indep_sets_pi_Union_Inter_of_disjoint
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → set (set Ω)}
{S T : set ι}
(h_indep : probability_theory.Indep_sets s μ)
(hST : disjoint S T) :
probability_theory.indep_sets (pi_Union_Inter s S) (pi_Union_Inter s T) μ
theorem
probability_theory.Indep_set.indep_generate_from_of_disjoint
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{s : ι → set Ω}
(hsm : ∀ (n : ι), measurable_set (s n))
(hs : probability_theory.Indep_set s μ)
(S T : set ι)
(hST : disjoint S 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 Ω}
[measure_theory.is_probability_measure μ]
{m : ι → measurable_space Ω}
(h_le : ∀ (i : ι), m i ≤ m0)
(h_indep : probability_theory.Indep m μ)
{S T : set ι}
(hST : disjoint S T) :
theorem
probability_theory.indep_supr_of_directed_le
{ι : Type u_2}
{Ω : Type u_1}
{m : ι → measurable_space Ω}
{m' m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(h_indep : ∀ (i : ι), probability_theory.indep (m i) m' μ)
(h_le : ∀ (i : ι), m i ≤ m0)
(h_le' : m' ≤ m0)
(hm : directed has_le.le 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 ι]
[measure_theory.is_probability_measure μ]
{s : ι → set Ω}
(hsm : ∀ (n : ι), measurable_set (s n))
(hs : probability_theory.Indep_set s μ)
(i : ι) :
probability_theory.indep (measurable_space.generate_from {s 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 ι]
[measure_theory.is_probability_measure μ]
{s : ι → set Ω}
(hsm : ∀ (n : ι), measurable_set (s n))
(hs : probability_theory.Indep_set s μ)
(i : ι)
{k : ι}
(hk : i < k) :
probability_theory.indep (measurable_space.generate_from {s 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 Ω}
[measure_theory.is_probability_measure μ]
{s : ℕ → set Ω}
(hsm : ∀ (n : ℕ), measurable_set (s n))
(hs : probability_theory.Indep_set s μ)
(n : ℕ) :
probability_theory.indep (measurable_space.generate_from {s (n + 1)}) (measurable_space.generate_from {t : set Ω | ∃ (k : ℕ) (H : k ≤ n), s k = t}) μ
theorem
probability_theory.indep_supr_of_monotone
{ι : Type u_2}
[semilattice_sup ι]
{Ω : Type u_1}
{m : ι → measurable_space Ω}
{m' m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(h_indep : ∀ (i : ι), probability_theory.indep (m 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}
[semilattice_inf ι]
{Ω : Type u_1}
{m : ι → measurable_space Ω}
{m' m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(h_indep : ∀ (i : ι), probability_theory.indep (m 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 : probability_theory.Indep_sets π μ)
(haS : a ∉ S) :
probability_theory.indep_sets (pi_Union_Inter π ↑S) (π a) μ
theorem
probability_theory.Indep_sets.Indep
{Ω : Type u_1}
{ι : Type u_2}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(m : ι → measurable_space Ω)
(h_le : ∀ (i : ι), m i ≤ m0)
(π : ι → set (set Ω))
(h_pi : ∀ (n : ι), is_pi_system (π n))
(h_generate : ∀ (i : ι), m i = measurable_space.generate_from (π i))
(h_ind : probability_theory.Indep_sets π μ) :
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)
(μ : measure_theory.measure Ω . "volume_tac")
[measure_theory.is_probability_measure μ] :
probability_theory.indep_set s t μ ↔ probability_theory.indep_sets {s} {t} μ
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)
(μ : measure_theory.measure Ω . "volume_tac")
[measure_theory.is_probability_measure μ] :
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)
(μ : measure_theory.measure Ω . "volume_tac")
[measure_theory.is_probability_measure μ]
(h_indep : probability_theory.indep_sets S T μ) :
theorem
probability_theory.indep.indep_set_of_measurable_set
{Ω : Type u_1}
{m₁ m₂ m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
(h_indep : probability_theory.indep m₁ m₂ μ)
{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 Ω) :
probability_theory.indep m₁ m₂ μ ↔ ∀ (s t : set Ω), measurable_set s → measurable_set t → probability_theory.indep_set s t μ
theorem
probability_theory.Indep_sets.meas_Inter
{Ω : Type u_1}
{ι : Type u_2}
{π : ι → set (set Ω)}
{f : ι → set Ω}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[fintype ι]
(h : probability_theory.Indep_sets π μ)
(hf : ∀ (i : ι), f i ∈ π i) :
theorem
probability_theory.Indep_comap_mem_iff
{Ω : Type u_1}
{ι : Type u_2}
{f : ι → set Ω}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω} :
probability_theory.Indep (λ (i : ι), measurable_space.comap (λ (_x : Ω), _x ∈ f i) ⊤) μ ↔ probability_theory.Indep_set f μ
theorem
probability_theory.Indep_set.Indep_comap_mem
{Ω : Type u_1}
{ι : Type u_2}
{f : ι → set Ω}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω} :
probability_theory.Indep_set f μ → probability_theory.Indep (λ (i : ι), measurable_space.comap (λ (_x : Ω), _x ∈ f i) ⊤) μ
Alias of the reverse direction of probability_theory.Indep_comap_mem_iff.
theorem
probability_theory.Indep_sets_singleton_iff
{Ω : Type u_1}
{ι : Type u_2}
{f : ι → set Ω}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω} :
theorem
probability_theory.Indep_set_iff_Indep_sets_singleton
{Ω : Type u_1}
{ι : Type u_2}
{f : ι → set Ω}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(hf : ∀ (i : ι), measurable_set (f i)) :
probability_theory.Indep_set f μ ↔ probability_theory.Indep_sets (λ (i : ι), {f i}) μ
theorem
probability_theory.Indep_set_iff_measure_Inter_eq_prod
{Ω : Type u_1}
{ι : Type u_2}
{f : ι → set Ω}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(hf : ∀ (i : ι), measurable_set (f i)) :
theorem
probability_theory.Indep_sets.Indep_set_of_mem
{Ω : Type u_1}
{ι : Type u_2}
{π : ι → set (set Ω)}
{f : ι → set Ω}
{m0 : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
(hfπ : ∀ (i : ι), f i ∈ π i)
(hf : ∀ (i : ι), measurable_set (f i))
(hπ : probability_theory.Indep_sets π μ) :
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 β'} :
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) :
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 β'}
[measure_theory.is_probability_measure μ]
(hf : measurable f)
(hg : measurable g) :
probability_theory.indep_fun f g μ ↔ ∀ (s : set β) (t : set β'), measurable_set s → measurable_set t → probability_theory.indep_set (f ⁻¹' s) (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 : probability_theory.indep_fun f g μ) :
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 : probability_theory.indep_fun f g μ)
(hf : f =ᵐ[μ] f')
(hg : g =ᵐ[μ] g') :
probability_theory.indep_fun f' 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 : probability_theory.indep_fun f g μ)
(hφ : measurable φ)
(hψ : measurable ψ) :
probability_theory.indep_fun (φ ∘ f) (ψ ∘ g) μ
theorem
probability_theory.Indep_fun.indep_fun_finset
{Ω : Type u_1}
{mΩ : measurable_space Ω}
{μ : measure_theory.measure Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
{β : ι → Type u_3}
{m : Π (i : ι), measurable_space (β i)}
{f : Π (i : ι), Ω → β i}
(S T : finset ι)
(hST : disjoint S T)
(hf_Indep : probability_theory.Indep_fun m f μ)
(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 Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
{β : ι → Type u_3}
{m : Π (i : ι), measurable_space (β i)}
{f : Π (i : ι), Ω → β i}
(hf_Indep : probability_theory.Indep_fun m f μ)
(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 Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
{β : Type u_3}
{m : measurable_space β}
[has_mul β]
[has_measurable_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 Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
{β : Type u_3}
{m : measurable_space β}
[has_add β]
[has_measurable_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 Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
{β : Type u_3}
{m : measurable_space β}
[add_comm_monoid β]
[has_measurable_add₂ β]
{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 Ω}
[measure_theory.is_probability_measure μ]
{ι : Type u_2}
{β : Type u_3}
{m : measurable_space β}
[comm_monoid β]
[has_measurable_mul₂ β]
{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 Ω}
[measure_theory.is_probability_measure μ]
{β : Type u_2}
{m : measurable_space β}
[comm_monoid β]
[has_measurable_mul₂ β]
{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 Ω}
[measure_theory.is_probability_measure μ]
{β : Type u_2}
{m : measurable_space β}
[add_comm_monoid β]
[has_measurable_add₂ β]
{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_set s μ) :
probability_theory.Indep_fun (λ (n : ι), m) (λ (n : ι), (s n).indicator (λ (ω : Ω), 1)) μ