theorem
ProbabilityTheory.Kernel.iIndepFun.finsets
{ι : Type u_1}
{α : Type u_2}
{Ω : Type u_7}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
{J : Type u_10}
[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_1}
{α : Type u_2}
{Ω : Type u_7}
{_mα : MeasurableSpace α}
{_mΩ : MeasurableSpace Ω}
{κ : ProbabilityTheory.Kernel α Ω}
{μ : MeasureTheory.Measure α}
{β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)}
{f : (i : ι) → Ω → β i}
{J : Type u_10}
[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_11)
{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.