Ω : Type u_1
ι✝ : Type ?u.3504903
β✝ : Type ?u.3504906
β' : Type ?u.3504909
γ : Type ?u.3504912
γ' : Type ?u.3504915
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝² : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω => (f i ω, f j ω)) (f k)
⊢ IndepFun (f i * f j) (f k)
Ω : Type u_1
ι✝ : Type ?u.3504903
β✝ : Type ?u.3504906
β' : Type ?u.3504909
γ : Type ?u.3504912
γ' : Type ?u.3504915
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝² : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (f i * f j) (f k)
have : IndepFun (fun ω => (f i ω, f j ω)) (f k) μ :=
  hf_Indep.indepFun_prod hf_meas i j k hik hjk
Ω : Type u_1
ι✝ : Type ?u.3504903
β✝ : Type ?u.3504906
β' : Type ?u.3504909
γ : Type ?u.3504912
γ' : Type ?u.3504915
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝² : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω => (f i ω, f j ω)) (f k)
⊢ IndepFun ((fun p => p.fst * p.snd) ∘ fun ω => (f i ω, f j ω)) (id ∘ f k)
Ω : Type u_1
ι✝ : Type ?u.3504903
β✝ : Type ?u.3504906
β' : Type ?u.3504909
γ : Type ?u.3504912
γ' : Type ?u.3504915
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝² : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω => (f i ω, f j ω)) (f k)
⊢ IndepFun (f i * f j) (f k)
change IndepFun ((fun p : β × β => p.fst * p.snd) ∘ fun ω => (f i ω, f j ω)) (id ∘ f k) μ
no goals
Ω : Type u_1
ι✝ : Type ?u.3504903
β✝ : Type ?u.3504906
β' : Type ?u.3504909
γ : Type ?u.3504912
γ' : Type ?u.3504915
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ : Ω → β✝
g : Ω → β'
inst✝² : IsProbabilityMeasure μ
ι : Type u_2
β : Type u_3
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (fun x => m) f
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω => (f i ω, f j ω)) (f k)
⊢ IndepFun ((fun p => p.fst * p.snd) ∘ fun ω => (f i ω, f j ω)) (id ∘ f k)
exact IndepFun.comp this (measurable_fst.mul measurable_snd) measurable_id