Conditional Independence #
We define conditional independence of sets/σ-algebras/functions with respect to a σ-algebra.
Two σ-algebras m₁
and m₂
are conditionally independent given a third σ-algebra m'
if for all
m₁
-measurable sets t₁
and m₂
-measurable sets t₂
,
μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧
.
On standard Borel spaces, the conditional expectation with respect to m'
defines a kernel
ProbabilityTheory.condexpKernel
, and the definition above is equivalent to
∀ᵐ ω ∂μ, condexpKernel μ m' ω (t₁ ∩ t₂) = condexpKernel μ m' ω t₁ * condexpKernel μ m' ω t₂
.
We use this property as the definition of conditional independence.
Main definitions #
We provide four definitions of conditional independence:
iCondIndepSets
: conditional independence of a family of sets of setspi : ι → Set (Set Ω)
. This is meant to be used with π-systems.iCondIndep
: conditional independence of a family of measurable space structuresm : ι → MeasurableSpace Ω
,iCondIndepSet
: conditional independence of a family of setss : ι → Set Ω
,iCondIndepFun
: conditional independence of a family of functions. For measurable spacesm : Π (i : ι), MeasurableSpace (β 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 the starting i
, for example CondIndepFun
is the version of
iCondIndepFun
for two functions.
Main statements #
ProbabilityTheory.iCondIndepSets.iCondIndep
: if π-systems are conditionally independent as sets of sets, then the measurable space structures they generate are conditionally independent.ProbabilityTheory.condIndepSets.condIndep
: variant with two π-systems.
Implementation notes #
The definitions of conditional independence in this file are a particular case of independence with
respect to a kernel and a measure, as defined in the file Probability/Independence/Kernel.lean
.
The kernel used is ProbabilityTheory.condexpKernel
.
A family of sets of sets π : ι → Set (Set Ω)
is conditionally independent given m'
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 | m'⟧ =ᵐ[μ] ∏ i ∈ s, μ⟦f i | m'⟧
.
See ProbabilityTheory.iCondIndepSets_iff
.
It will be used for families of pi_systems.
Equations
- ProbabilityTheory.iCondIndepSets m' hm' π μ = ProbabilityTheory.Kernel.iIndepSets π (ProbabilityTheory.condexpKernel μ m') (μ.trim hm')
Instances For
Two sets of sets s₁, s₂
are conditionally independent given m'
with respect to a measure
μ
if for any sets t₁ ∈ s₁, t₂ ∈ s₂
, then μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧
.
See ProbabilityTheory.condIndepSets_iff
.
Equations
- ProbabilityTheory.CondIndepSets m' hm' s1 s2 μ = ProbabilityTheory.Kernel.IndepSets s1 s2 (ProbabilityTheory.condexpKernel μ m') (μ.trim hm')
Instances For
A family of measurable space structures (i.e. of σ-algebras) is conditionally independent given
m'
with respect to a measure μ
(typically defined on a finer σ-algebra) if the family of sets of
measurable sets they define is independent. m : ι → MeasurableSpace Ω
is conditionally independent
given m'
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 | m'⟧ =ᵐ[μ] ∏ i ∈ s, μ⟦f i | m'⟧
.
See ProbabilityTheory.iCondIndep_iff
.
Equations
- ProbabilityTheory.iCondIndep m' hm' m μ = ProbabilityTheory.Kernel.iIndep m (ProbabilityTheory.condexpKernel μ m') (μ.trim hm')
Instances For
Two measurable space structures (or σ-algebras) m₁, m₂
are conditionally independent given
m'
with respect to a measure μ
(defined on a third σ-algebra) if for any sets
t₁ ∈ m₁, t₂ ∈ m₂
, μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧
.
See ProbabilityTheory.condIndep_iff
.
Equations
- ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ = ProbabilityTheory.Kernel.Indep m₁ m₂ (ProbabilityTheory.condexpKernel μ m') (μ.trim hm')
Instances For
A family of sets is conditionally independent if the family of measurable space structures they
generate is conditionally independent. For a set s
, the generated measurable space has measurable
sets ∅, s, sᶜ, univ
.
See ProbabilityTheory.iCondIndepSet_iff
.
Equations
- ProbabilityTheory.iCondIndepSet m' hm' s μ = ProbabilityTheory.Kernel.iIndepSet s (ProbabilityTheory.condexpKernel μ m') (μ.trim hm')
Instances For
Two sets are conditionally independent if the two measurable space structures they generate are
conditionally independent. For a set s
, the generated measurable space structure has measurable
sets ∅, s, sᶜ, univ
.
See ProbabilityTheory.condIndepSet_iff
.
Equations
- ProbabilityTheory.CondIndepSet m' hm' s t μ = ProbabilityTheory.Kernel.IndepSet s t (ProbabilityTheory.condexpKernel μ m') (μ.trim hm')
Instances For
A family of functions defined on the same space Ω
and taking values in possibly different
spaces, each with a measurable space structure, is conditionally independent if the family of
measurable space structures they generate on Ω
is conditionally independent. For a function g
with codomain having measurable space structure m
, the generated measurable space structure is
m.comap g
.
See ProbabilityTheory.iCondIndepFun_iff
.
Equations
- ProbabilityTheory.iCondIndepFun m' hm' m f μ = ProbabilityTheory.Kernel.iIndepFun m f (ProbabilityTheory.condexpKernel μ m') (μ.trim hm')
Instances For
Two functions are conditionally independent if the two measurable space structures they generate
are conditionally independent. For a function f
with codomain having measurable space structure
m
, the generated measurable space structure is m.comap f
.
See ProbabilityTheory.condIndepFun_iff
.
Equations
- ProbabilityTheory.CondIndepFun m' hm' f g μ = ProbabilityTheory.Kernel.IndepFun f g (ProbabilityTheory.condexpKernel μ m') (μ.trim hm')
Instances For
Deducing CondIndep
from iCondIndep
#
π-system lemma #
Conditional independence of measurable spaces is equivalent to conditional independence of generating π-systems.
Conditional independence of σ-algebras implies conditional independence of #
generating π-systems
Conditional independence of generating π-systems implies conditional independence of #
σ-algebras
The σ-algebras generated by conditionally independent pi-systems are conditionally independent.
Conditional independence of measurable sets #
Conditional independence of random variables #
If f
is a family of mutually conditionally independent random variables
(iCondIndepFun m' hm' m f μ
) and S, T
are two disjoint finite index sets, then the tuple formed
by f i
for i ∈ S
is conditionally independent of the tuple (f i)_i
for i ∈ T
.