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 ∈ 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.
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 Ω))
(κ : 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
- 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₁ 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
- 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 Ω)
(κ : 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
- 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 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
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)
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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 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 : Ω → γ)
(κ : Kernel α Ω)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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
@[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 μ
@[simp]
theorem
ProbabilityTheory.Kernel.iIndepFun_zero_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{β : ι → Type u_5}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (x : ι) → Ω → β x}
:
iIndepFun f κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indepFun_zero_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{β : Type u_5}
{γ : Type u_6}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
:
IndepFun f g κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indepFun_zero_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
{γ : Type u_6}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
:
IndepFun f g 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.iIndepFun_congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_5}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (x : ι) → Ω → β x}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_5}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (x : ι) → Ω → β x}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Alias of the forward direction of ProbabilityTheory.Kernel.iIndepFun_congr.
theorem
ProbabilityTheory.Kernel.indepFun_congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
{γ : Type u_6}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.IndepFun.congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
{γ : Type u_6}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Alias of the forward direction of ProbabilityTheory.Kernel.indepFun_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 κ μ
@[simp]
theorem
ProbabilityTheory.Kernel.iIndepFun.of_subsingleton
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[Subsingleton ι]
{β : ι → Type u_5}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
[IsMarkovKernel κ]
:
iIndepFun f κ μ
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : (x : ι) → Ω → β x}
(hf : iIndepFun f κ μ)
:
iIndep (fun (x : ι) => MeasurableSpace.comap (f x) (mβ x)) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : ι → Type u_4}
{mβ : (i : ι) → MeasurableSpace (β i)}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : (x : ι) → Ω → β x}
(h : iIndepFun f κ μ)
:
∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{S : Finset ι}
{f : (x : ι) → Ω → β x}
(hf : iIndepFun f κ μ)
(hs : ∀ i ∈ S, MeasurableSet (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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
{f : (x : ι) → Ω → β x}
[Fintype ι]
(hf : iIndepFun f κ μ)
(hs : ∀ (i : ι), MeasurableSet (s i))
:
theorem
ProbabilityTheory.Kernel.IndepFun.meas_inter
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
{γ : Type u_6}
[mβ : MeasurableSpace β]
[mγ : MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(hfg : IndepFun f g κ μ)
{s t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
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.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.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.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) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_4}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (i : ι) → Ω → β i}
(hf_Indep : iIndepFun f κ μ)
{i j : ι}
(hij : i ≠ j)
:
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 Ω}
{κ : 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_not_mem
{α : 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 α)
:
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
:
theorem
ProbabilityTheory.Kernel.IndepFun.measure_inter_preimage_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
:
Alias of the forward direction of ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul.
theorem
ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{ι : Type u_8}
{β : ι → Type u_9}
(m : (x : ι) → MeasurableSpace (β x))
(f : (i : ι) → Ω → β i)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.measure_inter_preimage_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{ι : Type u_8}
{β : ι → Type u_9}
(m : (x : ι) → MeasurableSpace (β x))
(f : (i : ι) → Ω → β i)
:
Alias of the forward direction of ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul.
theorem
ProbabilityTheory.Kernel.iIndepFun.congr'
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{mβ : (i : ι) → MeasurableSpace (β i)}
{f g : (i : ι) → Ω → β i}
(hf : iIndepFun f κ μ)
(h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i)
:
iIndepFun g κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.comp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{γ : ι → Type u_9}
{mβ : (i : ι) → MeasurableSpace (β i)}
{mγ : (i : ι) → MeasurableSpace (γ i)}
{f : (i : ι) → Ω → β i}
(h : iIndepFun f κ μ)
(g : (i : ι) → β i → γ i)
(hg : ∀ (i : ι), Measurable (g i))
:
theorem
ProbabilityTheory.Kernel.iIndepFun.comp₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{γ : ι → Type u_9}
{mβ : (i : ι) → MeasurableSpace (β i)}
{mγ : (i : ι) → MeasurableSpace (γ i)}
{f : (i : ι) → Ω → β i}
(h : iIndepFun f κ μ)
(g : (i : ι) → β i → γ i)
(hf : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(hg : ∀ (i : ι), AEMeasurable (g i) (MeasureTheory.Measure.map (f i) (μ.bind ⇑κ)))
:
theorem
ProbabilityTheory.Kernel.indepFun_iff_indepSet_preimage
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
[IsZeroOrMarkovKernel κ]
(hf : Measurable f)
(hg : Measurable g)
:
IndepFun f g κ μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → 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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{x✝ : MeasurableSpace β}
{x✝¹ : MeasurableSpace β'}
(hfg : IndepFun f g κ μ)
:
IndepFun g f κ μ
theorem
ProbabilityTheory.Kernel.IndepFun.congr'
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
{f' : Ω → β}
{g' : Ω → β'}
(hfg : IndepFun f g κ μ)
(hf : ∀ᵐ (a : α) ∂μ, f =ᵐ[κ a] f')
(hg : ∀ᵐ (a : α) ∂μ, g =ᵐ[κ a] g')
:
IndepFun f' g' κ μ
@[deprecated ProbabilityTheory.Kernel.IndepFun.congr' (since := "2025-03-18")]
theorem
ProbabilityTheory.Kernel.IndepFun.ae_eq
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
{f' : Ω → β}
{g' : Ω → β'}
(hfg : IndepFun f g κ μ)
(hf : ∀ᵐ (a : α) ∂μ, f =ᵐ[κ a] f')
(hg : ∀ᵐ (a : α) ∂μ, g =ᵐ[κ a] g')
:
IndepFun f' g' κ μ
Alias of ProbabilityTheory.Kernel.IndepFun.congr'.
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
{mγ : MeasurableSpace γ}
{mγ' : MeasurableSpace γ'}
{φ : β → γ}
{ψ : β' → γ'}
(hfg : IndepFun f g κ μ)
(hφ : Measurable φ)
(hψ : Measurable ψ)
:
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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
{mγ : MeasurableSpace γ}
{mγ' : MeasurableSpace γ'}
{φ : β → γ}
{ψ : β' → γ'}
(hfg : IndepFun f g κ μ)
(hf : AEMeasurable f (μ.bind ⇑κ))
(hg : AEMeasurable g (μ.bind ⇑κ))
(hφ : AEMeasurable φ (MeasureTheory.Measure.map f (μ.bind ⇑κ)))
(hψ : AEMeasurable ψ (MeasureTheory.Measure.map g (μ.bind ⇑κ)))
:
theorem
ProbabilityTheory.Kernel.IndepFun.neg_right
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{_mβ : MeasurableSpace β}
{_mβ' : MeasurableSpace β'}
[Neg β']
[MeasurableNeg β']
(hfg : IndepFun f g κ μ)
:
theorem
ProbabilityTheory.Kernel.IndepFun.neg_left
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{_mβ : MeasurableSpace β}
{_mβ' : MeasurableSpace β'}
[Neg β]
[MeasurableNeg β]
(hfg : IndepFun f g κ μ)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(S T : Finset ι)
(hST : Disjoint S T)
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
:
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_finset₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(S T : Finset ι)
(hST : Disjoint S T)
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
@[deprecated ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk (since := "2025-03-05")]
theorem
ProbabilityTheory.Kernel.ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
Alias of ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk.
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
@[deprecated ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk (since := "2025-03-05")]
theorem
ProbabilityTheory.Kernel.ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_mk_prod_mk
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
Alias of ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk.
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_right₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_add
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Mul β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_mul₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Add β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_left
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_left₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hik : i ≠ k)
(hjk : j ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_right₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k : ι)
(hij : i ≠ j)
(hik : i ≠ k)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_sub
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Div β]
[MeasurableDiv₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_div₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[Sub β]
[MeasurableSub₂ β]
{f : ι → Ω → β}
(hf_indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
(i j k l : ι)
(hik : i ≠ k)
(hil : i ≠ l)
(hjk : j ≠ k)
(hjl : j ≠ l)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_not_mem
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[CommMonoid β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
:
IndepFun (∏ j ∈ s, f j) (f i) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_not_mem
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[AddCommMonoid β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
:
IndepFun (∑ j ∈ s, 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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[CommMonoid β]
[MeasurableMul₂ β]
{f : ι → Ω → β}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
:
IndepFun (∏ j ∈ s, f j) (f i) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_not_mem₀
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[AddCommMonoid β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ))
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
:
IndepFun (∑ j ∈ s, f j) (f i) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[CommMonoid β]
[MeasurableMul₂ β]
{f : ℕ → Ω → β}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ℕ), Measurable (f i))
(n : ℕ)
:
IndepFun (∏ j ∈ Finset.range n, f j) (f n) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[AddCommMonoid β]
[MeasurableAdd₂ β]
{f : ℕ → Ω → β}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ℕ), Measurable (f i))
(n : ℕ)
:
IndepFun (∑ j ∈ Finset.range n, f j) (f n) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ₀
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[CommMonoid β]
[MeasurableMul₂ β]
{f : ℕ → Ω → β}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ℕ), AEMeasurable (f i) (μ.bind ⇑κ))
(n : ℕ)
:
IndepFun (∏ j ∈ Finset.range n, f j) (f n) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ₀
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[AddCommMonoid β]
[MeasurableAdd₂ β]
{f : ℕ → Ω → β}
(hf_Indep : iIndepFun f κ μ)
(hf_meas : ∀ (i : ℕ), AEMeasurable (f i) (μ.bind ⇑κ))
(n : ℕ)
:
IndepFun (∑ j ∈ Finset.range n, 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 Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
[Zero β]
[One β]
{m : MeasurableSpace β}
{s : ι → Set Ω}
(hs : iIndepSet s κ μ)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.cond_iInter
{ι : Type u_4}
{Ω : Type u_5}
{α : Type u_6}
{β : Type u_7}
{mΩ : MeasurableSpace Ω}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{X : ι → Ω → α}
{Y : ι → Ω → β}
{f : ι → Set Ω}
{t : ι → Set β}
{s : Finset ι}
[Finite ι]
(hY : ∀ (i : ι), Measurable (Y i))
(hindep : iIndepFun (fun (i : ι) (ω : Ω) => (X i ω, Y i ω)) κ μ)
(hf : ∀ i ∈ s, MeasurableSet (f i))
(hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0)
(ht : ∀ (i : ι), MeasurableSet (t i))
:
The probability of an intersection of preimages conditioning on another intersection factors into a product.