Independence of random variables with respect to a kernel and a measure #
A family of random variables is independent if the corresponding σ-algebras are independent.
Independence of families of sets and σ-algebras is covered in the Indep file.
This file deals with independence of random variables specifically.
Note that we define independence with respect to a kernel and a measure. 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.
Main definition #
ProbabilityTheory.Kernel.iIndepFun: independence of a family of functions (random variables). Variant for two functions:ProbabilityTheory.Kernel.IndepFun.
def
ProbabilityTheory.Kernel.iIndepFun
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mΩ : MeasurableSpace Ω}
{β : ι → Type u_8}
[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}
{β : Type u_4}
{γ : Type u_6}
{mα : MeasurableSpace α}
{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.iIndepFun_zero_right
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{β : ι → Type u_10}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (x : ι) → Ω → β x}
:
iIndepFun f κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indepFun_zero_right
{α : Type u_1}
{Ω : Type u_2}
{γ : Type u_6}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{β : Type u_10}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
:
IndepFun f g κ 0
@[simp]
theorem
ProbabilityTheory.Kernel.indepFun_zero_left
{α : Type u_1}
{Ω : Type u_2}
{γ : Type u_6}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_10}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
:
IndepFun f g 0 μ
theorem
ProbabilityTheory.Kernel.iIndepFun_congr
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_10}
{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_10}
{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}
{γ : Type u_6}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_10}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
theorem
ProbabilityTheory.Kernel.IndepFun.congr
{α : Type u_1}
{Ω : Type u_2}
{γ : Type u_6}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ η : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_10}
[MeasurableSpace β]
[MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(h : ⇑κ =ᵐ[μ] ⇑η)
:
Alias of the forward direction of ProbabilityTheory.Kernel.indepFun_congr.
@[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_10}
{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_8}
{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_8}
{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_8}
{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_8}
{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}
{γ : Type u_6}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : Type u_10}
[mβ : MeasurableSpace β]
[mγ : MeasurableSpace γ]
{f : Ω → β}
{g : Ω → γ}
(hfg : IndepFun f g κ μ)
{s t : Set Ω}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.precomp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : ι → Type u_8}
{mβ : (i : ι) → MeasurableSpace (β i)}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : (x : ι) → Ω → β x}
{ι' : Type u_9}
{g : ι' → ι}
(hg : Function.Injective g)
(h : iIndepFun f κ μ)
:
iIndepFun (fun (i : ι') => f (g i)) κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun.of_precomp
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : ι → Type u_8}
{mβ : (i : ι) → MeasurableSpace (β i)}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : (x : ι) → Ω → β x}
{ι' : Type u_9}
{g : ι' → ι}
(hg : Function.Surjective g)
(h : iIndepFun (fun (i : ι') => f (g i)) κ μ)
:
iIndepFun f κ μ
theorem
ProbabilityTheory.Kernel.iIndepFun_precomp_of_bijective
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : ι → Type u_8}
{mβ : (i : ι) → MeasurableSpace (β i)}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{f : (x : ι) → Ω → β x}
{ι' : Type u_9}
{g : ι' → ι}
(hg : Function.Bijective g)
:
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{mα : MeasurableSpace α}
{mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (x : ι) → MeasurableSpace (β x)}
{f : (i : ι) → Ω → β i}
(hf_Indep : iIndepFun f κ μ)
{i j : ι}
(hij : i ≠ j)
:
IndepFun (f i) (f j) κ μ
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_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}
(h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] 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)
(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' κ μ
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_const_left
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{mα : MeasurableSpace α}
{mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
[IsZeroOrMarkovKernel κ]
(c : β')
(X : Ω → β)
:
IndepFun (fun (x : Ω) => c) X κ μ
theorem
ProbabilityTheory.Kernel.indepFun_const_right
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{β' : Type u_5}
{mα : MeasurableSpace α}
{mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
[IsZeroOrMarkovKernel κ]
(X : Ω → β)
(c : β')
:
IndepFun X (fun (x : Ω) => c) κ μ
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.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map
{α : Type u_1}
{Ω : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{mα : MeasurableSpace α}
{mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
[MeasureTheory.IsFiniteMeasure μ]
[IsFiniteKernel κ]
{f : Ω → β}
{g : Ω → γ}
(hf : Measurable f)
(hg : Measurable g)
:
Two random variables f, g are independent given a kernel κ and a measure μ iff
μ ⊗ₘ κ.map (fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map 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))
:
IndepFun (fun (a : Ω) (i : ↥S) => f (↑i) a) (fun (a : Ω) (i : ↥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_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 ⇑κ))
:
IndepFun (fun (a : Ω) (i : ↥S) => f (↑i) a) (fun (a : Ω) (i : ↥T) => f (↑i) a) κ μ
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)
:
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)
:
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_notMem
{α : 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_notMem
{α : 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) κ μ
@[deprecated ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem (since := "2025-05-23")]
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) κ μ
Alias of ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem.
@[deprecated ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem (since := "2025-05-23")]
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) κ μ
Alias of ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem.
theorem
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem₀
{α : 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_notMem₀
{α : 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) κ μ
@[deprecated ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem₀ (since := "2025-05-23")]
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) κ μ
Alias of ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem₀.
@[deprecated ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem₀ (since := "2025-05-23")]
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) κ μ
Alias of ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem₀.
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_1}
{Ω : Type u_2}
{ι : Type u_3}
{β : Type u_4}
{mα : MeasurableSpace α}
{mΩ : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{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.