iIndepFun_iff_map_fun_eq_infinitePi_map

English

A variant ensuring conditional independence of a finite product of variables with respect to a single variable when the index is not in the Finset.

Русский

Вариант: для конечного произведения переменных и независимого индекса, произведение независимо от конкретной переменной.

LaTeX

$$$\forall s: Finset ι, \forall i \in ι, i \notin s \Rightarrow\; \text{CondIndepFun } m' hm' (s.prod (f)) (f i) μ.$$$

Lean4

/-- Random variables are independent iff their joint distribution is the product measure. -/
theorem iIndepFun_iff_map_fun_eq_infinitePi_map (mX : ∀ i, Measurable (X i)) :
    haveI _ i := isProbabilityMeasure_map (μ := μ) (mX i).aemeasurable
    iIndepFun X μ ↔ μ.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ μ.map (X i)) :=
  iIndepFun_iff_map_fun_eq_infinitePi_map₀ <| measurable_pi_iff.2 mX |>.aemeasurable

Похожие утверждения