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 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 α Ω)
(μ : 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 Ω))
(κ : ProbabilityTheory.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 Ω}
(κ : ProbabilityTheory.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 Ω}
(κ : ProbabilityTheory.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 Ω)
(κ : ProbabilityTheory.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 Ω)
(κ : ProbabilityTheory.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)
(κ : ProbabilityTheory.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 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 α Ω)
(μ : 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 Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{π : ι → Set (Set Ω)}
:
@[simp]
theorem
ProbabilityTheory.Kernel.indepSets_zero_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{s1 s2 : Set (Set Ω)}
:
ProbabilityTheory.Kernel.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 Ω)}
:
ProbabilityTheory.Kernel.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 Ω}
{κ : ProbabilityTheory.Kernel α Ω}
:
@[simp]
theorem
ProbabilityTheory.Kernel.indep_zero_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ m₂ _mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
:
ProbabilityTheory.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 Ω}
:
ProbabilityTheory.Kernel.Indep m₁ m₂ 0 μ
@[simp]
theorem
ProbabilityTheory.Kernel.iIndepSet_zero_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{s : ι → Set Ω}
:
@[simp]
theorem
ProbabilityTheory.Kernel.indepSet_zero_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{s t : Set Ω}
:
@[simp]
theorem
ProbabilityTheory.Kernel.indepSet_zero_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{s t : Set Ω}
:
@[simp]
theorem
ProbabilityTheory.Kernel.iIndepFun_zero_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{β : ι → Type u_5}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (x : ι) → Ω → β x}
:
@[simp]
theorem
ProbabilityTheory.Kernel.indepFun_zero_right
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{β : Type u_5}
{γ : Type u_6}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
:
@[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 : Ω → γ}
:
theorem
ProbabilityTheory.Kernel.iIndepSets_congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.iIndepSets.congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
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 Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s1 s2 : Set (Set Ω)}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.IndepSets s1 s2 κ μ ↔ ProbabilityTheory.Kernel.IndepSets s1 s2 η μ
theorem
ProbabilityTheory.Kernel.IndepSets.congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s1 s2 : Set (Set Ω)}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.IndepSets s1 s2 κ μ → ProbabilityTheory.Kernel.IndepSets s1 s2 η μ
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 Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.iIndep.congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.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 Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ ↔ ProbabilityTheory.Kernel.Indep m₁ m₂ η μ
theorem
ProbabilityTheory.Kernel.Indep.congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{m₁ m₂ _mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ → ProbabilityTheory.Kernel.Indep m₁ m₂ η μ
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 Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s : ι → Set Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.iIndepSet.congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.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 Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s t : Set Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.IndepSet s t κ μ ↔ ProbabilityTheory.Kernel.IndepSet s t η μ
theorem
ProbabilityTheory.Kernel.indepSet.congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{s t : Set Ω}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.IndepSet s t κ μ → ProbabilityTheory.Kernel.IndepSet s t η μ
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 Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_5}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (x : ι) → Ω → β x}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.iIndepFun m f κ μ ↔ ProbabilityTheory.Kernel.iIndepFun m f η μ
theorem
ProbabilityTheory.Kernel.iIndepFun.congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_5}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (x : ι) → Ω → β x}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.iIndepFun m f κ μ → ProbabilityTheory.Kernel.iIndepFun m f η μ
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 Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
{γ : Type u_6}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.IndepFun f g κ μ ↔ ProbabilityTheory.Kernel.IndepFun f g η μ
theorem
ProbabilityTheory.Kernel.IndepFun.congr
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_5}
{γ : Type u_6}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
ProbabilityTheory.Kernel.IndepFun f g κ μ → ProbabilityTheory.Kernel.IndepFun f g η μ
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 Ω}
{κ : 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) = ∏ i ∈ s, (κ a) (f i)
theorem
ProbabilityTheory.Kernel.iIndepSets.ae_isProbabilityMeasure
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{π : ι → Set (Set Ω)}
(h : ProbabilityTheory.Kernel.iIndepSets π κ μ)
:
∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
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) = ∏ 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.ae_isProbabilityMeasure
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h : ProbabilityTheory.Kernel.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 Ω}
{κ : 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) = ∏ i ∈ S, (κ 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) = ∏ 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.ae_isProbabilityMeasure
{α : 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}
(h : ProbabilityTheory.Kernel.iIndepFun mβ 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 Ω}
{κ : 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) = ∏ i ∈ S, (κ 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) = ∏ 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 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₁ 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₁ m₂ _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.IsZeroOrMarkovKernel κ]
:
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.IsZeroOrMarkovKernel κ]
:
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.IsZeroOrMarkovKernel κ]
(s : Set Ω)
:
theorem
ProbabilityTheory.Kernel.indepSet_empty_left
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.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 Ω}
{κ : 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₁ s₂ 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₁ m₂ m₃ _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₁ m₂ m₃ _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₁ s₂ 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₁ s₂ 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₁ 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) = ∏ i ∈ S, (κ a) (s i)
theorem
ProbabilityTheory.Kernel.indepSets_singleton_iff
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s 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 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₂ m : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
{p1 p2 : Set (Set Ω)}
(h2 : m₂ ≤ m)
(hp2 : IsPiSystem p2)
(hpm2 : m₂ = MeasurableSpace.generateFrom p2)
(hyp : ProbabilityTheory.Kernel.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 Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.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 : 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.IsZeroOrMarkovKernel κ]
{p1 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 α}
{s : ι → Set (Set Ω)}
{S 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 α}
{s : ι → Set Ω}
(hsm : ∀ (n : ι), MeasurableSet (s n))
(hs : ProbabilityTheory.Kernel.iIndepSet s κ μ)
(S 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 α}
{m : ι → MeasurableSpace Ω}
(h_le : ∀ (i : ι), m i ≤ _mΩ)
(h_indep : ProbabilityTheory.Kernel.iIndep m κ μ)
{S 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' m0 : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(h_indep : ∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ)
(h_le : ∀ (i : ι), m i ≤ m0)
(h_le' : m' ≤ m0)
(hm : Directed (fun (x1 x2 : MeasurableSpace Ω) => x1 ≤ x2) 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 ι]
{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 ι]
{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 α}
{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' m0 : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(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' m0 : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(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 α}
(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 α Ω}
{μ : MeasureTheory.Measure α}
{f : ι → Set Ω}
(hf : ∀ (i : ι), MeasurableSet (f i))
:
ProbabilityTheory.Kernel.iIndepSet f κ μ ↔ ProbabilityTheory.Kernel.iIndepSets (fun (i : ι) => {f i}) κ μ
theorem
ProbabilityTheory.Kernel.iIndepSet.meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : ι → Set Ω}
(h : ProbabilityTheory.Kernel.iIndepSet f κ μ)
(s : Finset ι)
:
∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
theorem
ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : ι → Set Ω}
(hf : ∀ (i : ι), MeasurableSet (f i))
:
ProbabilityTheory.Kernel.iIndepSet f κ μ ↔ ∀ (s : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ 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 α Ω}
{μ : 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 t : Set Ω}
{m0 : MeasurableSpace Ω}
(hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t)
(κ : ProbabilityTheory.Kernel α Ω)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
:
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 t : Set Ω}
{_m0 : MeasurableSpace Ω}
(hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t)
(κ : ProbabilityTheory.Kernel α Ω)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
:
ProbabilityTheory.Kernel.IndepSet s t κ μ ↔ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
theorem
ProbabilityTheory.Kernel.IndepSet.measure_inter_eq_mul
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{s t : Set Ω}
{_m0 : MeasurableSpace Ω}
(κ : ProbabilityTheory.Kernel α Ω)
(μ : MeasureTheory.Measure α)
(h : ProbabilityTheory.Kernel.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)
(κ : ProbabilityTheory.Kernel α Ω)
(μ : MeasureTheory.Measure α)
[ProbabilityTheory.IsZeroOrMarkovKernel κ]
(h_indep : ProbabilityTheory.Kernel.IndepSets S T κ μ)
:
theorem
ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m₁ m₂ x✝ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
(h_indep : ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ)
{s t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.indep_iff_forall_indepSet
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
(m₁ 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.IndepFun.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)
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 Ω}
{κ : 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) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
theorem
ProbabilityTheory.Kernel.iIndepFun.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)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
Alias of the forward direction of ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul.
theorem
ProbabilityTheory.Kernel.iIndepFun.comp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{γ : ι → Type u_9}
{mβ : (i : ι) → MeasurableSpace (β i)}
{mγ : (i : ι) → MeasurableSpace (γ i)}
{f : (i : ι) → Ω → β i}
(h : ProbabilityTheory.Kernel.iIndepFun mβ f κ μ)
(g : (i : ι) → β i → γ i)
(hg : ∀ (i : ι), Measurable (g i))
:
ProbabilityTheory.Kernel.iIndepFun mγ (fun (i : ι) => g i ∘ f 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.IsZeroOrMarkovKernel κ]
(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✝¹ : MeasurableSpace β'}
(hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ)
:
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 : α) ∂μ, f =ᵐ[κ a] f')
(hg : ∀ᵐ (a : α) ∂μ, g =ᵐ[κ a] 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.IndepFun.neg_right
{α : 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 β'}
[Neg β']
[MeasurableNeg β']
(hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ)
:
ProbabilityTheory.Kernel.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 Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : Ω → β}
{g : Ω → β'}
{_mβ : MeasurableSpace β}
{_mβ' : MeasurableSpace β'}
[Neg β]
[MeasurableNeg β]
(hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ)
:
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.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}
(S 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}
(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}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(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_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 : ι → Ω → β}
(hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
:
ProbabilityTheory.Kernel.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 Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[AddCommMonoid β]
[MeasurableAdd₂ β]
{f : ι → Ω → β}
(hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ι) => m) f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{s : Finset ι}
{i : ι}
(hi : i ∉ s)
:
ProbabilityTheory.Kernel.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 Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[CommMonoid β]
[MeasurableMul₂ β]
{f : ℕ → Ω → β}
(hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ℕ) => m) f κ μ)
(hf_meas : ∀ (i : ℕ), Measurable (f i))
(n : ℕ)
:
ProbabilityTheory.Kernel.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 Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_8}
{m : MeasurableSpace β}
[AddCommMonoid β]
[MeasurableAdd₂ β]
{f : ℕ → Ω → β}
(hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun (x : ℕ) => m) f κ μ)
(hf_meas : ∀ (i : ℕ), Measurable (f i))
(n : ℕ)
:
ProbabilityTheory.Kernel.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 Ω}
{κ : 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) κ μ