Independence with respect to a kernel and a measure #
A family of sets of sets π : ι → Set (Set Ω) is independent with respect to a kernel
κ : kernel α Ω and a measure μ on α 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 for μ-almost every a : α,
κ a (⋂ i in s, f i) = ∏ i in s, κ a (f i).
This notion of independence is a generalization of both independence and conditional independence.
For conditional independence, κ is the conditional kernel ProbabilityTheory.condexpKernel and
μ is the ambiant measure. For (non-conditional) independence, κ = kernel.const Unit μ and the
measure is the Dirac measure on Unit.
The main purpose of this file is to prove only once the properties that hold for both conditional and non-conditional independence.
Main definitions #
ProbabilityTheory.kernel.iIndepSets: independence of a family of sets of sets. Variant for two sets of sets:ProbabilityTheory.kernel.IndepSets.ProbabilityTheory.kernel.iIndep: independence of a family of σ-algebras. Variant for two σ-algebras:Indep.ProbabilityTheory.kernel.iIndepSet: independence of a family of sets. Variant for two sets:ProbabilityTheory.kernel.IndepSet.ProbabilityTheory.kernel.iIndepFun: independence of a family of functions (random variables). Variant for two functions:ProbabilityTheory.kernel.IndepFun.
See the file Mathlib/Probability/Kernel/Basic.lean for a more detailed discussion of these
definitions in the particular case of the usual independence notion.
Main statements #
ProbabilityTheory.kernel.iIndepSets.iIndep: if π-systems are independent as sets of sets, then the measurable space structures they generate are independent.ProbabilityTheory.kernel.IndepSets.Indep: variant with two π-systems.
def
ProbabilityTheory.kernel.iIndepSets
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
(π : ι → Set (Set Ω))
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
A family of sets of sets π : ι → Set (Set Ω) is independent with respect to a kernel κ and
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 ∀ᵐ a ∂μ, κ a (⋂ i in s, f i) = ∏ i in s, κ a (f i).
It will be used for families of pi_systems.
Equations
Instances For
def
ProbabilityTheory.kernel.IndepSets
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
(s1 : Set (Set Ω))
(s2 : Set (Set Ω))
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
Two sets of sets s₁, s₂ are independent with respect to a kernel κ and a measure μ if for
any sets t₁ ∈ s₁, t₂ ∈ s₂, then ∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)
Equations
Instances For
def
ProbabilityTheory.kernel.iIndep
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
(m : ι → MeasurableSpace Ω)
{_mΩ : MeasurableSpace Ω}
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a
kernel κ and a measure μ if the family of sets of measurable sets they define is independent.
Equations
- ProbabilityTheory.kernel.iIndep m κ μ = ProbabilityTheory.kernel.iIndepSets (fun (x : ι) => {s : Set Ω | MeasurableSet s}) κ μ
Instances For
def
ProbabilityTheory.kernel.Indep
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m₁ : MeasurableSpace Ω)
(m₂ : MeasurableSpace Ω)
{_mΩ : MeasurableSpace Ω}
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
Two measurable space structures (or σ-algebras) m₁, m₂ are independent with respect to a
kernel κ and a measure μ if for any sets t₁ ∈ m₁, t₂ ∈ m₂,
∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a (t₁) * κ a (t₂)
Equations
- ProbabilityTheory.kernel.Indep m₁ m₂ κ μ = ProbabilityTheory.kernel.IndepSets {s : Set Ω | MeasurableSet s} {s : Set Ω | MeasurableSet s} κ μ
Instances For
def
ProbabilityTheory.kernel.iIndepSet
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
(s : ι → Set Ω)
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
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
- ProbabilityTheory.kernel.iIndepSet s κ μ = ProbabilityTheory.kernel.iIndep (fun (i : ι) => MeasurableSpace.generateFrom {s i}) κ μ
Instances For
def
ProbabilityTheory.kernel.IndepSet
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
(s : Set Ω)
(t : Set Ω)
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
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
Instances For
def
ProbabilityTheory.kernel.iIndepFun
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{β : ι → Type u_4}
(m : (x : ι) → MeasurableSpace (β x))
(f : (x : ι) → Ω → β x)
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
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 MeasurableSpace.comap g m.
Equations
- ProbabilityTheory.kernel.iIndepFun m f κ μ = ProbabilityTheory.kernel.iIndep (fun (x : ι) => MeasurableSpace.comap (f x) (m x)) κ μ
Instances For
def
ProbabilityTheory.kernel.IndepFun
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{β : Type u_4}
{γ : Type u_5}
{_mΩ : MeasurableSpace Ω}
[mβ : MeasurableSpace β]
[mγ : MeasurableSpace γ]
(f : Ω → β)
(g : Ω → γ)
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
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 MeasurableSpace.comap f m.
Equations
- ProbabilityTheory.kernel.IndepFun f g κ μ = ProbabilityTheory.kernel.Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) κ μ
Instances For
theorem
ProbabilityTheory.kernel.iIndepSets.meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
(h : ProbabilityTheory.kernel.iIndepSets π κ μ)
(s : Finset ι)
{f : ι → Set Ω}
(hf : ∀ i ∈ s, f i ∈ π i)
:
∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ i ∈ s, f i) = s.prod fun (i : ι) => ↑↑(κ a) (f i)
theorem
ProbabilityTheory.kernel.iIndepSets.meas_iInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{s : ι → Set Ω}
[Fintype ι]
(h : ProbabilityTheory.kernel.iIndepSets π κ μ)
(hs : ∀ (i : ι), s i ∈ π i)
:
∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ (i : ι), s i) = Finset.univ.prod fun (i : ι) => ↑↑(κ a) (s i)
theorem
ProbabilityTheory.kernel.iIndep.iIndepSets'
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(hμ : ProbabilityTheory.kernel.iIndep m κ μ)
:
ProbabilityTheory.kernel.iIndepSets (fun (x : ι) => {s : Set Ω | MeasurableSet s}) κ μ
theorem
ProbabilityTheory.kernel.iIndep.meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{S : Finset ι}
(hμ : ProbabilityTheory.kernel.iIndep m κ μ)
(hs : ∀ i ∈ S, MeasurableSet (s i))
:
∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ i ∈ S, s i) = S.prod fun (i : ι) => ↑↑(κ a) (s i)
theorem
ProbabilityTheory.kernel.iIndep.meas_iInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
[Fintype ι]
(h : ProbabilityTheory.kernel.iIndep m κ μ)
(hs : ∀ (i : ι), MeasurableSet (s i))
:
∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ (i : ι), s i) = Finset.univ.prod fun (i : ι) => ↑↑(κ a) (s i)
theorem
ProbabilityTheory.kernel.iIndepFun.iIndep
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : ι → Type u_4}
{mβ : (i : ι) → MeasurableSpace (β i)}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{f : (x : ι) → Ω → β x}
(hf : ProbabilityTheory.kernel.iIndepFun mβ f κ μ)
:
ProbabilityTheory.kernel.iIndep (fun (x : ι) => MeasurableSpace.comap (f x) (mβ x)) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : ι → Type u_4}
{mβ : (i : ι) → MeasurableSpace (β i)}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{S : Finset ι}
{f : (x : ι) → Ω → β x}
(hf : ProbabilityTheory.kernel.iIndepFun mβ f κ μ)
(hs : ∀ i ∈ S, MeasurableSet (s i))
:
∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ i ∈ S, s i) = S.prod fun (i : ι) => ↑↑(κ a) (s i)
theorem
ProbabilityTheory.kernel.iIndepFun.meas_iInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : ι → Type u_4}
{mβ : (i : ι) → MeasurableSpace (β i)}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{f : (x : ι) → Ω → β x}
[Fintype ι]
(hf : ProbabilityTheory.kernel.iIndepFun mβ f κ μ)
(hs : ∀ (i : ι), MeasurableSet (s i))
:
∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ (i : ι), s i) = Finset.univ.prod fun (i : ι) => ↑↑(κ a) (s i)
theorem
ProbabilityTheory.kernel.IndepFun.meas_inter
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
{γ : Type u_6}
[mβ : MeasurableSpace β]
[mγ : MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(hfg : ProbabilityTheory.kernel.IndepFun f g κ μ)
{s : Set Ω}
{t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.kernel.IndepSets.symm
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{s₁ : Set (Set Ω)}
{s₂ : Set (Set Ω)}
(h : ProbabilityTheory.kernel.IndepSets s₁ s₂ κ μ)
:
ProbabilityTheory.kernel.IndepSets s₂ s₁ κ μ
theorem
ProbabilityTheory.kernel.Indep.symm
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ : MeasurableSpace Ω}
{m₂ : MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h : ProbabilityTheory.kernel.Indep m₁ m₂ κ μ)
:
ProbabilityTheory.kernel.Indep m₂ m₁ κ μ
theorem
ProbabilityTheory.kernel.indep_bot_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m' : MeasurableSpace Ω)
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.kernel.Indep m' ⊥ κ μ
theorem
ProbabilityTheory.kernel.indep_bot_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m' : MeasurableSpace Ω)
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.kernel.Indep ⊥ m' κ μ
theorem
ProbabilityTheory.kernel.indepSet_empty_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
(s : Set Ω)
:
theorem
ProbabilityTheory.kernel.indepSet_empty_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
(s : Set Ω)
:
theorem
ProbabilityTheory.kernel.indepSets_of_indepSets_of_le_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ : Set (Set Ω)}
{s₂ : Set (Set Ω)}
{s₃ : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h_indep : ProbabilityTheory.kernel.IndepSets s₁ s₂ κ μ)
(h31 : s₃ ⊆ s₁)
:
ProbabilityTheory.kernel.IndepSets s₃ s₂ κ μ
theorem
ProbabilityTheory.kernel.indepSets_of_indepSets_of_le_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ : Set (Set Ω)}
{s₂ : Set (Set Ω)}
{s₃ : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h_indep : ProbabilityTheory.kernel.IndepSets s₁ s₂ κ μ)
(h32 : s₃ ⊆ s₂)
:
ProbabilityTheory.kernel.IndepSets s₁ s₃ κ μ
theorem
ProbabilityTheory.kernel.indep_of_indep_of_le_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ : MeasurableSpace Ω}
{m₂ : MeasurableSpace Ω}
{m₃ : MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h_indep : ProbabilityTheory.kernel.Indep m₁ m₂ κ μ)
(h31 : m₃ ≤ m₁)
:
ProbabilityTheory.kernel.Indep m₃ m₂ κ μ
theorem
ProbabilityTheory.kernel.indep_of_indep_of_le_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ : MeasurableSpace Ω}
{m₂ : MeasurableSpace Ω}
{m₃ : MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h_indep : ProbabilityTheory.kernel.Indep m₁ m₂ κ μ)
(h32 : m₃ ≤ m₂)
:
ProbabilityTheory.kernel.Indep m₁ m₃ κ μ
theorem
ProbabilityTheory.kernel.IndepSets.union
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ : Set (Set Ω)}
{s₂ : Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h₁ : ProbabilityTheory.kernel.IndepSets s₁ s' κ μ)
(h₂ : ProbabilityTheory.kernel.IndepSets s₂ s' κ μ)
:
ProbabilityTheory.kernel.IndepSets (s₁ ∪ s₂) s' κ μ
@[simp]
theorem
ProbabilityTheory.kernel.IndepSets.union_iff
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ : Set (Set Ω)}
{s₂ : Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
:
ProbabilityTheory.kernel.IndepSets (s₁ ∪ s₂) s' κ μ ↔ ProbabilityTheory.kernel.IndepSets s₁ s' κ μ ∧ ProbabilityTheory.kernel.IndepSets s₂ s' κ μ
theorem
ProbabilityTheory.kernel.IndepSets.iUnion
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(hyp : ∀ (n : ι), ProbabilityTheory.kernel.IndepSets (s n) s' κ μ)
:
ProbabilityTheory.kernel.IndepSets (⋃ (n : ι), s n) s' κ μ
theorem
ProbabilityTheory.kernel.IndepSets.bUnion
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{u : Set ι}
(hyp : ∀ n ∈ u, ProbabilityTheory.kernel.IndepSets (s n) s' κ μ)
:
ProbabilityTheory.kernel.IndepSets (⋃ n ∈ u, s n) s' κ μ
theorem
ProbabilityTheory.kernel.IndepSets.inter
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ : Set (Set Ω)}
{s' : Set (Set Ω)}
(s₂ : Set (Set Ω))
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h₁ : ProbabilityTheory.kernel.IndepSets s₁ s' κ μ)
:
ProbabilityTheory.kernel.IndepSets (s₁ ∩ s₂) s' κ μ
theorem
ProbabilityTheory.kernel.IndepSets.iInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h : ∃ (n : ι), ProbabilityTheory.kernel.IndepSets (s n) s' κ μ)
:
ProbabilityTheory.kernel.IndepSets (⋂ (n : ι), s n) s' κ μ
theorem
ProbabilityTheory.kernel.IndepSets.bInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{u : Set ι}
(h : ∃ n ∈ u, ProbabilityTheory.kernel.IndepSets (s n) s' κ μ)
:
ProbabilityTheory.kernel.IndepSets (⋂ n ∈ u, s n) s' κ μ
theorem
ProbabilityTheory.kernel.iIndep_comap_mem_iff
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{f : ι → Set Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
:
ProbabilityTheory.kernel.iIndep (fun (i : ι) => MeasurableSpace.comap (fun (x : Ω) => x ∈ f i) ⊤) κ μ ↔ ProbabilityTheory.kernel.iIndepSet f κ μ
theorem
ProbabilityTheory.kernel.iIndepSets_singleton_iff
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
:
ProbabilityTheory.kernel.iIndepSets (fun (i : ι) => {s i}) κ μ ↔ ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ i ∈ S, s i) = S.prod fun (i : ι) => ↑↑(κ a) (s i)
theorem
ProbabilityTheory.kernel.indepSets_singleton_iff
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s : Set Ω}
{t : Set Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
:
ProbabilityTheory.kernel.IndepSets {s} {t} κ μ ↔ ∀ᵐ (a : α) ∂μ, ↑↑(κ a) (s ∩ t) = ↑↑(κ a) s * ↑↑(κ a) t
theorem
ProbabilityTheory.kernel.iIndepSets.indepSets
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h_indep : ProbabilityTheory.kernel.iIndepSets s κ μ)
{i : ι}
{j : ι}
(hij : i ≠ j)
:
ProbabilityTheory.kernel.IndepSets (s i) (s j) κ μ
theorem
ProbabilityTheory.kernel.iIndep.indep
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h_indep : ProbabilityTheory.kernel.iIndep m κ μ)
{i : ι}
{j : ι}
(hij : i ≠ j)
:
ProbabilityTheory.kernel.Indep (m i) (m j) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_4}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (i : ι) → Ω → β i}
(hf_Indep : ProbabilityTheory.kernel.iIndepFun m f κ μ)
{i : ι}
{j : ι}
(hij : i ≠ j)
:
ProbabilityTheory.kernel.IndepFun (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
ProbabilityTheory.kernel.iIndep.iIndepSets
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{m : ι → MeasurableSpace Ω}
{s : ι → Set (Set Ω)}
(hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n))
(h_indep : ProbabilityTheory.kernel.iIndep m κ μ)
:
theorem
ProbabilityTheory.kernel.Indep.indepSets
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{s1 : Set (Set Ω)}
{s2 : Set (Set Ω)}
(h_indep : ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) κ μ)
:
ProbabilityTheory.kernel.IndepSets s1 s2 κ μ
Independence of generating π-systems implies independence of measurable space structures #
theorem
ProbabilityTheory.kernel.IndepSets.indep_aux
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₂ : MeasurableSpace Ω}
{m : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{p1 : Set (Set Ω)}
{p2 : Set (Set Ω)}
(h2 : m₂ ≤ m)
(hp2 : IsPiSystem p2)
(hpm2 : m₂ = MeasurableSpace.generateFrom p2)
(hyp : ProbabilityTheory.kernel.IndepSets p1 p2 κ μ)
{t1 : Set Ω}
{t2 : Set Ω}
(ht1 : t1 ∈ p1)
(ht1m : MeasurableSet t1)
(ht2m : MeasurableSet t2)
:
theorem
ProbabilityTheory.kernel.IndepSets.indep
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m1 : MeasurableSpace Ω}
{m2 : MeasurableSpace Ω}
{m : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{p1 : Set (Set Ω)}
{p2 : Set (Set Ω)}
(h1 : m1 ≤ m)
(h2 : m2 ≤ m)
(hp1 : IsPiSystem p1)
(hp2 : IsPiSystem p2)
(hpm1 : m1 = MeasurableSpace.generateFrom p1)
(hpm2 : m2 = MeasurableSpace.generateFrom p2)
(hyp : ProbabilityTheory.kernel.IndepSets p1 p2 κ μ)
:
ProbabilityTheory.kernel.Indep m1 m2 κ μ
The measurable space structures generated by independent pi-systems are independent.
theorem
ProbabilityTheory.kernel.IndepSets.indep'
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{p1 : Set (Set Ω)}
{p2 : Set (Set Ω)}
(hp1m : ∀ s ∈ p1, MeasurableSet s)
(hp2m : ∀ s ∈ p2, MeasurableSet s)
(hp1 : IsPiSystem p1)
(hp2 : IsPiSystem p2)
(hyp : ProbabilityTheory.kernel.IndepSets p1 p2 κ μ)
:
theorem
ProbabilityTheory.kernel.indepSets_piiUnionInter_of_disjoint
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → Set (Set Ω)}
{S : Set ι}
{T : Set ι}
(h_indep : ProbabilityTheory.kernel.iIndepSets s κ μ)
(hST : Disjoint S T)
:
ProbabilityTheory.kernel.IndepSets (piiUnionInter s S) (piiUnionInter s T) κ μ
theorem
ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_of_disjoint
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → Set Ω}
(hsm : ∀ (n : ι), MeasurableSet (s n))
(hs : ProbabilityTheory.kernel.iIndepSet s κ μ)
(S : Set ι)
(T : Set ι)
(hST : Disjoint S T)
:
ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom {t : Set Ω | ∃ n ∈ S, s n = t})
(MeasurableSpace.generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
theorem
ProbabilityTheory.kernel.indep_iSup_of_disjoint
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{m : ι → MeasurableSpace Ω}
(h_le : ∀ (i : ι), m i ≤ _mΩ)
(h_indep : ProbabilityTheory.kernel.iIndep m κ μ)
{S : Set ι}
{T : Set ι}
(hST : Disjoint S T)
:
ProbabilityTheory.kernel.Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
theorem
ProbabilityTheory.kernel.indep_iSup_of_directed_le
{α : Type u_1}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{Ω : Type u_4}
{m : ι → MeasurableSpace Ω}
{m' : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
(h_indep : ∀ (i : ι), ProbabilityTheory.kernel.Indep (m i) m' κ μ)
(h_le : ∀ (i : ι), m i ≤ m0)
(h_le' : m' ≤ m0)
(hm : Directed (fun (x x_1 : MeasurableSpace Ω) => x ≤ x_1) m)
:
ProbabilityTheory.kernel.Indep (⨆ (i : ι), m i) m' κ μ
theorem
ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_lt
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → Set Ω}
(hsm : ∀ (n : ι), MeasurableSet (s n))
(hs : ProbabilityTheory.kernel.iIndepSet s κ μ)
(i : ι)
:
ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom {s i})
(MeasurableSpace.generateFrom {t : Set Ω | ∃ j < i, s j = t}) κ μ
theorem
ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_le
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[LinearOrder ι]
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → Set Ω}
(hsm : ∀ (n : ι), MeasurableSet (s n))
(hs : ProbabilityTheory.kernel.iIndepSet s κ μ)
(i : ι)
{k : ι}
(hk : i < k)
:
ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom {s k})
(MeasurableSpace.generateFrom {t : Set Ω | ∃ j ≤ i, s j = t}) κ μ
theorem
ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_le_nat
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ℕ → Set Ω}
(hsm : ∀ (n : ℕ), MeasurableSet (s n))
(hs : ProbabilityTheory.kernel.iIndepSet s κ μ)
(n : ℕ)
:
ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom {s (n + 1)})
(MeasurableSpace.generateFrom {t : Set Ω | ∃ k ≤ n, s k = t}) κ μ
theorem
ProbabilityTheory.kernel.indep_iSup_of_monotone
{α : Type u_1}
{ι : Type u_3}
{_mα : MeasurableSpace α}
[SemilatticeSup ι]
{Ω : Type u_4}
{m : ι → MeasurableSpace Ω}
{m' : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
(h_indep : ∀ (i : ι), ProbabilityTheory.kernel.Indep (m i) m' κ μ)
(h_le : ∀ (i : ι), m i ≤ m0)
(h_le' : m' ≤ m0)
(hm : Monotone m)
:
ProbabilityTheory.kernel.Indep (⨆ (i : ι), m i) m' κ μ
theorem
ProbabilityTheory.kernel.indep_iSup_of_antitone
{α : Type u_1}
{ι : Type u_3}
{_mα : MeasurableSpace α}
[SemilatticeInf ι]
{Ω : Type u_4}
{m : ι → MeasurableSpace Ω}
{m' : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
(h_indep : ∀ (i : ι), ProbabilityTheory.kernel.Indep (m i) m' κ μ)
(h_le : ∀ (i : ι), m i ≤ m0)
(h_le' : m' ≤ m0)
(hm : Antitone m)
:
ProbabilityTheory.kernel.Indep (⨆ (i : ι), m i) m' κ μ
theorem
ProbabilityTheory.kernel.iIndepSets.piiUnionInter_of_not_mem
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{a : ι}
{S : Finset ι}
(hp_ind : ProbabilityTheory.kernel.iIndepSets π κ μ)
(haS : a ∉ S)
:
ProbabilityTheory.kernel.IndepSets (piiUnionInter π ↑S) (π a) κ μ
theorem
ProbabilityTheory.kernel.iIndepSets.iIndep
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
(m : ι → MeasurableSpace Ω)
(h_le : ∀ (i : ι), m i ≤ _mΩ)
(π : ι → Set (Set Ω))
(h_pi : ∀ (n : ι), IsPiSystem (π n))
(h_generate : ∀ (i : ι), m i = MeasurableSpace.generateFrom (π i))
(h_ind : ProbabilityTheory.kernel.iIndepSets π κ μ)
:
The measurable space structures generated by independent pi-systems are independent.
Independence of measurable sets #
We prove the following equivalences on IndepSet, for measurable sets s, t.
theorem
ProbabilityTheory.kernel.iIndepSet_iff_iIndepSets_singleton
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
[ProbabilityTheory.IsMarkovKernel κ]
{μ : MeasureTheory.Measure α}
{f : ι → Set Ω}
(hf : ∀ (i : ι), MeasurableSet (f i))
:
ProbabilityTheory.kernel.iIndepSet f κ μ ↔ ProbabilityTheory.kernel.iIndepSets (fun (i : ι) => {f i}) κ μ
theorem
ProbabilityTheory.kernel.iIndepSet_iff_meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
[ProbabilityTheory.IsMarkovKernel κ]
{μ : MeasureTheory.Measure α}
{f : ι → Set Ω}
(hf : ∀ (i : ι), MeasurableSet (f i))
:
ProbabilityTheory.kernel.iIndepSet f κ μ ↔ ∀ (s : Finset ι), ∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ i ∈ s, f i) = s.prod fun (i : ι) => ↑↑(κ a) (f i)
theorem
ProbabilityTheory.kernel.iIndepSets.iIndepSet_of_mem
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
[ProbabilityTheory.IsMarkovKernel κ]
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{f : ι → Set Ω}
(hfπ : ∀ (i : ι), f i ∈ π i)
(hf : ∀ (i : ι), MeasurableSet (f i))
(hπ : ProbabilityTheory.kernel.iIndepSets π κ μ)
:
theorem
ProbabilityTheory.kernel.indepSet_iff_indepSets_singleton
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s : Set Ω}
{t : Set Ω}
{m0 : MeasurableSpace Ω}
(hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t)
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.kernel.IndepSet s t κ μ ↔ ProbabilityTheory.kernel.IndepSets {s} {t} κ μ
theorem
ProbabilityTheory.kernel.indepSet_iff_measure_inter_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s : Set Ω}
{t : Set Ω}
{_m0 : MeasurableSpace Ω}
(hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t)
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsMarkovKernel κ]
:
ProbabilityTheory.kernel.IndepSet s t κ μ ↔ ∀ᵐ (a : α) ∂μ, ↑↑(κ a) (s ∩ t) = ↑↑(κ a) s * ↑↑(κ a) t
theorem
ProbabilityTheory.kernel.IndepSets.indepSet_of_mem
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s : Set Ω}
{t : Set Ω}
(S : Set (Set Ω))
(T : Set (Set Ω))
{_m0 : MeasurableSpace Ω}
(hs : s ∈ S)
(ht : t ∈ T)
(hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t)
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsMarkovKernel κ]
(h_indep : ProbabilityTheory.kernel.IndepSets S T κ μ)
:
theorem
ProbabilityTheory.kernel.Indep.indepSet_of_measurableSet
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ : MeasurableSpace Ω}
{m₂ : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
(h_indep : ProbabilityTheory.kernel.Indep m₁ m₂ κ μ)
{s : Set Ω}
{t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.kernel.indep_iff_forall_indepSet
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m₁ : MeasurableSpace Ω)
(m₂ : MeasurableSpace Ω)
{_m0 : MeasurableSpace Ω}
(κ : ↥(ProbabilityTheory.kernel α Ω))
(μ : MeasureTheory.Measure α)
:
ProbabilityTheory.kernel.Indep m₁ m₂ κ μ ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → ProbabilityTheory.kernel.IndepSet s t κ μ
Independence of random variables #
theorem
ProbabilityTheory.kernel.indepFun_iff_measure_inter_preimage_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
:
ProbabilityTheory.kernel.IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'),
MeasurableSet s →
MeasurableSet t → ∀ᵐ (a : α) ∂μ, ↑↑(κ a) (f ⁻¹' s ∩ g ⁻¹' t) = ↑↑(κ a) (f ⁻¹' s) * ↑↑(κ a) (g ⁻¹' t)
theorem
ProbabilityTheory.kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{ι : Type u_8}
{β : ι → Type u_9}
(m : (x : ι) → MeasurableSpace (β x))
(f : (i : ι) → Ω → β i)
:
ProbabilityTheory.kernel.iIndepFun m f κ μ ↔ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
(∀ i ∈ S, MeasurableSet (sets i)) →
∀ᵐ (a : α) ∂μ, ↑↑(κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = S.prod fun (i : ι) => ↑↑(κ a) (f i ⁻¹' sets i)
theorem
ProbabilityTheory.kernel.indepFun_iff_indepSet_preimage
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
[ProbabilityTheory.IsMarkovKernel κ]
(hf : Measurable f)
(hg : Measurable g)
:
ProbabilityTheory.kernel.IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'),
MeasurableSet s → MeasurableSet t → ProbabilityTheory.kernel.IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
theorem
ProbabilityTheory.kernel.IndepFun.symm
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
:
∀ {x : MeasurableSpace β} {x_1 : MeasurableSpace β'},
ProbabilityTheory.kernel.IndepFun f g κ μ → ProbabilityTheory.kernel.IndepFun g f κ μ
theorem
ProbabilityTheory.kernel.IndepFun.ae_eq
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
{f' : Ω → β}
{g' : Ω → β'}
(hfg : ProbabilityTheory.kernel.IndepFun f g κ μ)
(hf : ∀ᵐ (a : α) ∂μ, (κ a).ae.EventuallyEq f f')
(hg : ∀ᵐ (a : α) ∂μ, (κ a).ae.EventuallyEq g g')
:
ProbabilityTheory.kernel.IndepFun f' g' κ μ
theorem
ProbabilityTheory.kernel.IndepFun.comp
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{γ : Type u_6}
{γ' : Type u_7}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
{mγ : MeasurableSpace γ}
{mγ' : MeasurableSpace γ'}
{φ : β → γ}
{ψ : β' → γ'}
(hfg : ProbabilityTheory.kernel.IndepFun f g κ μ)
(hφ : Measurable φ)
(hψ : Measurable ψ)
:
ProbabilityTheory.kernel.IndepFun (φ ∘ f) (ψ ∘ g) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.of_subsingleton
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
[ProbabilityTheory.IsMarkovKernel κ]
[Subsingleton ι]
:
theorem
ProbabilityTheory.kernel.iIndepFun.ae_isProbabilityMeasure
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(h : ProbabilityTheory.kernel.iIndepFun m f κ μ)
:
∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_finset
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
[ProbabilityTheory.IsMarkovKernel κ]
(S : Finset ι)
(T : Finset ι)
(hST : Disjoint S T)
(hf_Indep : ProbabilityTheory.kernel.iIndepFun m f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
:
ProbabilityTheory.kernel.IndepFun (fun (a : Ω) (i : { x : ι // x ∈ S }) => f (↑i) a)
(fun (a : Ω) (i : { x : ι // x ∈ T }) => f (↑i) a) κ μ
If f is a family of mutually independent random variables (iIndepFun 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
ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_Indep : ProbabilityTheory.kernel.iIndepFun m f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
ProbabilityTheory.kernel.IndepFun (fun (a : Ω) => (f i a, f j a)) (f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk_prod_mk
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun m f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
ProbabilityTheory.kernel.IndepFun (fun (a : Ω) => (f i a, f j a)) (fun (a : Ω) => (f k a, f l a)) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_add_left
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
ProbabilityTheory.kernel.IndepFun (f i + f j) (f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_mul_left
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
ProbabilityTheory.kernel.IndepFun (f i * f j) (f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_add_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
ProbabilityTheory.kernel.IndepFun (f i) (f j + f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_mul_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
ProbabilityTheory.kernel.IndepFun (f i) (f j * f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_add_add
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
ProbabilityTheory.kernel.IndepFun (f i + f j) (f k + f l) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_mul_mul
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
ProbabilityTheory.kernel.IndepFun (f i * f j) (f k * f l) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_sub_left
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
ProbabilityTheory.kernel.IndepFun (f i - f j) (f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_div_left
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
ProbabilityTheory.kernel.IndepFun (f i / f j) (f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_sub_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
ProbabilityTheory.kernel.IndepFun (f i) (f j - f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_div_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
ProbabilityTheory.kernel.IndepFun (f i) (f j / f k) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_sub_sub
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
ProbabilityTheory.kernel.IndepFun (f i - f j) (f k - f l) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_div_div
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i : ι)
(j : ι)
(k : ι)
(l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
ProbabilityTheory.kernel.IndepFun (f i / f j) (f k / f l) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_finset_sum_of_not_mem
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[AddCommMonoid β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
:
ProbabilityTheory.kernel.IndepFun (s.sum fun (j : ι) => f j) (f i) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_finset_prod_of_not_mem
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[CommMonoid β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
[ProbabilityTheory.IsMarkovKernel κ]
(hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
:
ProbabilityTheory.kernel.IndepFun (s.prod fun (j : ι) => f j) (f i) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_sum_range_succ
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[AddCommMonoid β]
[MeasurableAdd₂ β]
[ProbabilityTheory.IsMarkovKernel κ]
{f : ℕ → Ω → β}
(hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ℕ) => m) f κ μ)
(hf_meas : ∀ (i : ℕ), Measurable (f i))
(n : ℕ)
:
ProbabilityTheory.kernel.IndepFun ((Finset.range n).sum fun (j : ℕ) => f j) (f n) κ μ
theorem
ProbabilityTheory.kernel.iIndepFun.indepFun_prod_range_succ
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[CommMonoid β]
[MeasurableMul₂ β]
[ProbabilityTheory.IsMarkovKernel κ]
{f : ℕ → Ω → β}
(hf_Indep : ProbabilityTheory.kernel.iIndepFun (fun (x : ℕ) => m) f κ μ)
(hf_meas : ∀ (i : ℕ), Measurable (f i))
(n : ℕ)
:
ProbabilityTheory.kernel.IndepFun ((Finset.range n).prod fun (j : ℕ) => f j) (f n) κ μ
theorem
ProbabilityTheory.kernel.iIndepSet.iIndepFun_indicator
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : Type u_4}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
[Zero β]
[One β]
{m : MeasurableSpace β}
{s : ι → Set Ω}
(hs : ProbabilityTheory.kernel.iIndepSet s κ μ)
:
ProbabilityTheory.kernel.iIndepFun (fun (_n : ι) => m) (fun (n : ι) => (s n).indicator fun (_ω : Ω) => 1) κ μ