theorem
ProbabilityTheory.kernel.IndepFun.ae_eq'
{α : Type u_6}
{Ω : Type u_5}
{β : Type u_1}
{β' : Type u_2}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
{f : Ω → β}
{f' : Ω → β}
{g : Ω → β'}
{g' : Ω → β'}
(hfg : ProbabilityTheory.kernel.IndepFun f g κ μ)
(hf : ∀ᵐ (a : α) ∂μ, (κ a).ae.EventuallyEq f f')
(hg : ∀ᵐ (a : α) ∂μ, (κ a).ae.EventuallyEq g g')
:
ProbabilityTheory.kernel.IndepFun f' g' κ μ
in mathlib as of 4d385393cd569f08ac30425ef886a57bb10daaa5 (TODO: bump)
theorem
ProbabilityTheory.kernel.iIndepFun.comp
{α : Type u_9}
{Ω : Type u_8}
{ι : Type u_7}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_5}
{γ : ι → Type u_6}
{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.iIndepFun.finsets
{α : Type u_9}
{Ω : Type u_8}
{ι : Type u_10}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_5}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
[ProbabilityTheory.IsMarkovKernel κ]
{J : Type u_7}
[Fintype J]
(S : J → Finset ι)
(h_disjoint : Set.univ.PairwiseDisjoint S)
(hf_Indep : ProbabilityTheory.kernel.iIndepFun m f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
:
ProbabilityTheory.kernel.iIndepFun (fun (x : J) => MeasurableSpace.pi)
(fun (j : J) (a : Ω) (i : { x : ι // x ∈ S j }) => f (↑i) a) κ μ
If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint
finite index sets, then the tuples formed by f i for i ∈ S j are mutually independent,
when seen as a family indexed by J.
theorem
ProbabilityTheory.kernel.iIndepFun.finsets_comp
{α : Type u_10}
{Ω : Type u_9}
{ι : Type u_11}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_5}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
[ProbabilityTheory.IsMarkovKernel κ]
{J : Type u_7}
[Fintype J]
(S : J → Finset ι)
(h_disjoint : Set.univ.PairwiseDisjoint S)
(hf_Indep : ProbabilityTheory.kernel.iIndepFun m f κ μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(γ : J → Type u_8)
{mγ : (j : J) → MeasurableSpace (γ j)}
(φ : (j : J) → ((i : { x : ι // x ∈ S j }) → β ↑i) → γ j)
(hφ : ∀ (j : J), Measurable (φ j))
:
ProbabilityTheory.kernel.iIndepFun mγ (fun (j : J) (a : Ω) => φ j fun (i : { x : ι // x ∈ S j }) => f (↑i) a) κ μ
If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint
finite index sets, and φ j is a function that maps the tuple formed by f i for i ∈ S j to a
measurable space γ j, then the family of random variables formed by φ j (f i)_{i ∈ S j} and
indexed by J is iIndep.