English
Let (f_i) be iIndepFun μ and each f_i measurable. Then the finite product over a set s of indices is independent of f_i for any i not in s.
Русский
Пусть (f_i) — iIndepFun μ и каждая f_i измерима. Тогда конечное произведение по множеству индексов s независимо от f_i, если i ∉ s.
LaTeX
$$$\\forall s\\ I\\ lbrace i\\rbrace,\\ Not(i \\in s) \\Rightarrow IndepFun(\\prod_{j \\in s} f_j, f_i)\\mu$$$
Lean4
theorem cond [Finite ι] (hY : ∀ i, Measurable (Y i)) (hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ)
(hy : ∀ i, μ (Y i ⁻¹' t i) ≠ 0) (ht : ∀ i, MeasurableSet (t i)) : iIndepFun X μ[|⋂ i, Y i ⁻¹' t i] :=
by
rw [iIndepFun_iff]
intro s f hf
convert cond_iInter hY hindep hf (fun i _ ↦ hy _) ht using 2 with i hi
simpa using cond_iInter hY hindep (fun j hj ↦ hf _ <| Finset.mem_singleton.1 hj ▸ hi) (fun i _ ↦ hy _) ht
