Independence of families of sets 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 ∈ 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 ambient 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.
This file contains results about independence of families of sets and σ-algebras.
See the IndepFun file for results about independence of random variables.
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.
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 Ω))
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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 ∈ 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 s2 : Set (Set Ω))
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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 Ω}
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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
Instances For
def
ProbabilityTheory.Kernel.Indep
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m₁ m₂ : MeasurableSpace Ω)
{_mΩ : MeasurableSpace Ω}
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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
Instances For
def
ProbabilityTheory.Kernel.iIndepSet
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
(s : ι → Set Ω)
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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
Instances For
def
ProbabilityTheory.Kernel.IndepSet
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
(s t : Set Ω)
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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
@[simp]
theorem
ProbabilityTheory.Kernel.iIndepSets_zero_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{π : ι → Set (Set Ω)}
:
iIndepSets π κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indepSets_zero_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{s1 s2 : Set (Set Ω)}
:
IndepSets s1 s2 κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indepSets_zero_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{s1 s2 : Set (Set Ω)}
:
IndepSets s1 s2 0 μ
@[simp]
theorem
ProbabilityTheory.Kernel.iIndep_zero_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
:
iIndep m κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indep_zero_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ m₂ _mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
:
Indep m₁ m₂ κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indep_zero_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{m₁ m₂ _mΩ : MeasurableSpace Ω}
:
Indep m₁ m₂ 0 μ
@[simp]
theorem
ProbabilityTheory.Kernel.iIndepSet_zero_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{s : ι → Set Ω}
:
iIndepSet s κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indepSet_zero_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{s t : Set Ω}
:
IndepSet s t κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indepSet_zero_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{s t : Set Ω}
:
IndepSet s t 0 μ
theorem
ProbabilityTheory.Kernel.iIndepSets_congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.iIndepSets.congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
iIndepSets π κ μ → iIndepSets π η μ
Alias of the forward direction of ProbabilityTheory.Kernel.iIndepSets_congr.
theorem
ProbabilityTheory.Kernel.indepSets_congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s1 s2 : Set (Set Ω)}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.IndepSets.congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s1 s2 : Set (Set Ω)}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Alias of the forward direction of ProbabilityTheory.Kernel.indepSets_congr.
theorem
ProbabilityTheory.Kernel.iIndep_congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.iIndep.congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Alias of the forward direction of ProbabilityTheory.Kernel.iIndep_congr.
theorem
ProbabilityTheory.Kernel.indep_congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{m₁ m₂ _mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.Indep.congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{m₁ m₂ _mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Alias of the forward direction of ProbabilityTheory.Kernel.indep_congr.
theorem
ProbabilityTheory.Kernel.iIndepSet_congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.iIndepSet.congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Alias of the forward direction of ProbabilityTheory.Kernel.iIndepSet_congr.
theorem
ProbabilityTheory.Kernel.indepSet_congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s t : Set Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.indepSet.congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s t : Set Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Alias of the forward direction of ProbabilityTheory.Kernel.indepSet_congr.
theorem
ProbabilityTheory.Kernel.iIndepSets.meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
(h : iIndepSets π κ μ)
(s : Finset ι)
{f : ι → Set Ω}
(hf : ∀ i ∈ s, f i ∈ π i)
:
theorem
ProbabilityTheory.Kernel.iIndepSets.ae_isProbabilityMeasure
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
(h : iIndepSets π κ μ)
:
∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
theorem
ProbabilityTheory.Kernel.iIndepSets.meas_iInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{s : ι → Set Ω}
[Fintype ι]
(h : iIndepSets π κ μ)
(hs : ∀ (i : ι), s i ∈ π i)
:
theorem
ProbabilityTheory.Kernel.iIndep.iIndepSets'
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(hμ : iIndep m κ μ)
:
Kernel.iIndepSets (fun (x : ι) => {s : Set Ω | MeasurableSet s}) κ μ
theorem
ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h : iIndep m κ μ)
:
∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
theorem
ProbabilityTheory.Kernel.iIndep.meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{S : Finset ι}
(hμ : iIndep m κ μ)
(hs : ∀ i ∈ S, MeasurableSet (s i))
:
theorem
ProbabilityTheory.Kernel.iIndep.meas_iInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
[Fintype ι]
(h : iIndep m κ μ)
(hs : ∀ (i : ι), MeasurableSet (s i))
:
@[simp]
theorem
ProbabilityTheory.Kernel.iIndepSets.of_subsingleton
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
[Subsingleton ι]
{m : ι → Set (Set Ω)}
{κ : Kernel α Ω}
[IsMarkovKernel κ]
:
iIndepSets m κ μ
@[simp]
theorem
ProbabilityTheory.Kernel.iIndep.of_subsingleton
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
[Subsingleton ι]
{m : ι → MeasurableSpace Ω}
{κ : Kernel α Ω}
[IsMarkovKernel κ]
:
iIndep m κ μ
theorem
ProbabilityTheory.Kernel.iIndepSets.precomp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Injective g)
(h : iIndepSets π κ μ)
:
iIndepSets (π ∘ g) κ μ
theorem
ProbabilityTheory.Kernel.iIndepSets.of_precomp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Surjective g)
(h : iIndepSets (π ∘ g) κ μ)
:
iIndepSets π κ μ
theorem
ProbabilityTheory.Kernel.iIndepSets_precomp_of_bijective
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Bijective g)
:
theorem
ProbabilityTheory.Kernel.iIndep.precomp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Injective g)
(h : iIndep m κ μ)
:
theorem
ProbabilityTheory.Kernel.iIndep.of_precomp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Surjective g)
(h : iIndep (m ∘ g) κ μ)
:
iIndep m κ μ
theorem
ProbabilityTheory.Kernel.iIndep_precomp_of_bijective
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Bijective g)
:
theorem
ProbabilityTheory.Kernel.iIndepSet.precomp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Injective g)
(h : iIndepSet s κ μ)
:
theorem
ProbabilityTheory.Kernel.iIndepSet.of_precomp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Surjective g)
(h : iIndepSet (s ∘ g) κ μ)
:
iIndepSet s κ μ
theorem
ProbabilityTheory.Kernel.iIndepSet_precomp_of_bijective
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{ι' : Type u_5}
{g : ι' → ι}
(hg : Function.Bijective g)
:
theorem
ProbabilityTheory.Kernel.IndepSets.symm
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set (Set Ω)}
(h : IndepSets s₁ s₂ κ μ)
:
IndepSets s₂ s₁ κ μ
theorem
ProbabilityTheory.Kernel.Indep.symm
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ m₂ _mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h : Indep m₁ m₂ κ μ)
:
Indep m₂ m₁ κ μ
theorem
ProbabilityTheory.Kernel.indep_bot_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m' : MeasurableSpace Ω)
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
:
theorem
ProbabilityTheory.Kernel.indep_bot_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m' : MeasurableSpace Ω)
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
:
theorem
ProbabilityTheory.Kernel.indepSet_empty_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
(s : Set Ω)
:
theorem
ProbabilityTheory.Kernel.indepSet_empty_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
(s : Set Ω)
:
theorem
ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ s₂ s₃ : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : IndepSets s₁ s₂ κ μ)
(h31 : s₃ ⊆ s₁)
:
IndepSets s₃ s₂ κ μ
theorem
ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ s₂ s₃ : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : IndepSets s₁ s₂ κ μ)
(h32 : s₃ ⊆ s₂)
:
IndepSets s₁ s₃ κ μ
theorem
ProbabilityTheory.Kernel.indep_of_indep_of_le_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ m₂ m₃ _mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : Indep m₁ m₂ κ μ)
(h31 : m₃ ≤ m₁)
:
Indep m₃ m₂ κ μ
theorem
ProbabilityTheory.Kernel.indep_of_indep_of_le_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ m₂ m₃ _mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : Indep m₁ m₂ κ μ)
(h32 : m₃ ≤ m₂)
:
Indep m₁ m₃ κ μ
theorem
ProbabilityTheory.Kernel.iIndep_of_iIndep_of_le
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m₁ m₂ : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : iIndep m₂ κ μ)
(h_le : ∀ (i : ι), m₁ i ≤ m₂ i)
:
iIndep m₁ κ μ
theorem
ProbabilityTheory.Kernel.IndepSets.union
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ s₂ s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h₁ : IndepSets s₁ s' κ μ)
(h₂ : IndepSets s₂ s' κ μ)
:
@[simp]
theorem
ProbabilityTheory.Kernel.IndepSets.union_iff
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ s₂ s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
:
theorem
ProbabilityTheory.Kernel.IndepSets.iUnion
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(hyp : ∀ (n : ι), IndepSets (s n) s' κ μ)
:
IndepSets (⋃ (n : ι), s n) s' κ μ
theorem
ProbabilityTheory.Kernel.IndepSets.biUnion
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{u : Set ι}
(hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ)
:
IndepSets (⋃ n ∈ u, s n) s' κ μ
@[deprecated ProbabilityTheory.Kernel.IndepSets.biUnion (since := "2025-11-02")]
theorem
ProbabilityTheory.Kernel.IndepSets.bUnion
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{u : Set ι}
(hyp : ∀ n ∈ u, IndepSets (s n) s' κ μ)
:
IndepSets (⋃ n ∈ u, s n) s' κ μ
theorem
ProbabilityTheory.Kernel.IndepSets.inter
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s₁ s' : Set (Set Ω)}
(s₂ : Set (Set Ω))
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h₁ : IndepSets 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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h : ∃ (n : ι), IndepSets (s n) s' κ μ)
:
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{u : Set ι}
(h : ∃ n ∈ u, IndepSets (s n) s' κ μ)
:
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
:
theorem
ProbabilityTheory.Kernel.iIndepSets_singleton_iff
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
:
theorem
ProbabilityTheory.Kernel.indepSets_singleton_iff
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s t : Set Ω}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
:
theorem
ProbabilityTheory.Kernel.iIndepSets.indepSets
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → Set (Set Ω)}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : iIndepSets s κ μ)
{i j : ι}
(hij : i ≠ j)
:
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : iIndep m κ μ)
{i j : ι}
(hij : i ≠ j)
:
Indep (m i) (m j) κ μ
π-system lemma #
Independence of measurable spaces is equivalent to independence of generating π-systems.
Independence of measurable space structures implies independence of generating π-systems #
theorem
ProbabilityTheory.Kernel.iIndep.iIndepSets
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{m : ι → MeasurableSpace Ω}
{s : ι → Set (Set Ω)}
(hms : ∀ (n : ι), m n = MeasurableSpace.generateFrom (s n))
(h_indep : iIndep m κ μ)
:
Kernel.iIndepSets s κ μ
theorem
ProbabilityTheory.Kernel.Indep.indepSets
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s1 s2 : Set (Set Ω)}
(h_indep : Indep (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) κ μ)
:
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₂ m : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
{p1 p2 : Set (Set Ω)}
(h2 : m₂ ≤ m)
(hp2 : IsPiSystem p2)
(hpm2 : m₂ = MeasurableSpace.generateFrom p2)
(hyp : IndepSets p1 p2 κ μ)
{t1 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 m2 m : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
{p1 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 : IndepSets p1 p2 κ μ)
:
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
{p1 p2 : Set (Set Ω)}
(hp1m : ∀ s ∈ p1, MeasurableSet s)
(hp2m : ∀ s ∈ p2, MeasurableSet s)
(hp1 : IsPiSystem p1)
(hp2 : IsPiSystem p2)
(hyp : IndepSets p1 p2 κ μ)
:
Indep (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) κ μ
theorem
ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set (Set Ω)}
{S T : Set ι}
(h_indep : iIndepSets s κ μ)
(hST : Disjoint S T)
:
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
(hsm : ∀ (n : ι), MeasurableSet (s n))
(hs : iIndepSet s κ μ)
(S T : Set ι)
(hST : Disjoint S T)
:
theorem
ProbabilityTheory.Kernel.indep_iSup_of_disjoint
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{m : ι → MeasurableSpace Ω}
(h_le : ∀ (i : ι), m i ≤ _mΩ)
(h_indep : iIndep m κ μ)
{S T : Set ι}
(hST : Disjoint S T)
:
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' m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
(h_indep : ∀ (i : ι), Indep (m i) m' κ μ)
(h_le : ∀ (i : ι), m i ≤ m0)
(h_le' : m' ≤ m0)
(hm : Directed (fun (x1 x2 : MeasurableSpace Ω) => x1 ≤ x2) m)
:
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[Preorder ι]
{s : ι → Set Ω}
(hsm : ∀ (n : ι), MeasurableSet (s n))
(hs : iIndepSet s κ μ)
(i : ι)
:
theorem
ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[Preorder ι]
{s : ι → Set Ω}
(hsm : ∀ (n : ι), MeasurableSet (s n))
(hs : iIndepSet s κ μ)
(i : ι)
{k : ι}
(hk : i < k)
:
theorem
ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le_nat
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ℕ → Set Ω}
(hsm : ∀ (n : ℕ), MeasurableSet (s n))
(hs : iIndepSet s κ μ)
(n : ℕ)
:
theorem
ProbabilityTheory.Kernel.indep_iSup_of_monotone
{α : Type u_1}
{ι : Type u_3}
{_mα : MeasurableSpace α}
[SemilatticeSup ι]
{Ω : Type u_4}
{m : ι → MeasurableSpace Ω}
{m' m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
(h_indep : ∀ (i : ι), Indep (m i) m' κ μ)
(h_le : ∀ (i : ι), m i ≤ m0)
(h_le' : m' ≤ m0)
(hm : Monotone m)
:
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' m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[IsZeroOrMarkovKernel κ]
(h_indep : ∀ (i : ι), Indep (m i) m' κ μ)
(h_le : ∀ (i : ι), m i ≤ m0)
(h_le' : m' ≤ m0)
(hm : Antitone m)
:
Indep (⨆ (i : ι), m i) m' κ μ
theorem
ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{a : ι}
{S : Finset ι}
(hp_ind : iIndepSets π κ μ)
(haS : a ∉ S)
:
IndepSets (piiUnionInter π ↑S) (π a) κ μ
theorem
ProbabilityTheory.Kernel.iIndepSets.iIndep
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(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 : iIndepSets π κ μ)
:
Kernel.iIndep m κ μ
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : ι → Set Ω}
(hf : ∀ (i : ι), MeasurableSet (f i))
:
theorem
ProbabilityTheory.Kernel.iIndepSet.meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : ι → Set Ω}
(h : iIndepSet f κ μ)
(s : Finset ι)
:
theorem
ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : ι → Set Ω}
(hf : ∀ (i : ι), MeasurableSet (f i))
:
theorem
ProbabilityTheory.Kernel.iIndepSets.iIndepSet_of_mem
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
{f : ι → Set Ω}
(hfπ : ∀ (i : ι), f i ∈ π i)
(hf : ∀ (i : ι), MeasurableSet (f i))
(hπ : iIndepSets π κ μ)
:
iIndepSet f κ μ
theorem
ProbabilityTheory.Kernel.indepSet_iff_indepSets_singleton
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s t : Set Ω}
{m0 : MeasurableSpace Ω}
(hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t)
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α)
[IsZeroOrMarkovKernel κ]
:
theorem
ProbabilityTheory.Kernel.indepSet_iff_measure_inter_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s t : Set Ω}
{_m0 : MeasurableSpace Ω}
(hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t)
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α)
[IsZeroOrMarkovKernel κ]
:
theorem
ProbabilityTheory.Kernel.IndepSet.measure_inter_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s t : Set Ω}
{_m0 : MeasurableSpace Ω}
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α)
(h : IndepSet s t κ μ)
:
theorem
ProbabilityTheory.Kernel.IndepSets.indepSet_of_mem
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s t : Set Ω}
(S T : Set (Set Ω))
{_m0 : MeasurableSpace Ω}
(hs : s ∈ S)
(ht : t ∈ T)
(hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t)
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α)
[IsZeroOrMarkovKernel κ]
(h_indep : IndepSets S T κ μ)
:
IndepSet s t κ μ
theorem
ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ m₂ x✝ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : Indep m₁ m₂ κ μ)
{s t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
IndepSet s t κ μ
theorem
ProbabilityTheory.Kernel.indep_iff_forall_indepSet
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m₁ m₂ : MeasurableSpace Ω)
{_m0 : MeasurableSpace Ω}
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α)
: