English
Conditioning on an intersection of events Y_i preimages yields a product form for the conditional probabilities given the intersection.
Русский
Условие на пересечение событий в виде условий на предобразы даёт произведение условных вероятностей.
LaTeX
$$$\\mu[\\bigcap_i( f_i) \\\\| \\\\bigcap_i Y_i^{-1} t_i] = \\prod_i \\mu[f_i \\\\| Y_i \\in t_i]$$$
Lean4
/-- A finite number of random variables are independent if and only if their joint characteristic
function is equal to the product of the characteristic functions.
This is `iIndepFun_iff_charFunDual_pi` for `WithLp`. See `iIndepFun_iff_charFun_pi` for the
Hilbert space version. -/
theorem iIndepFun_iff_charFunDual_pi' (hX : ∀ i, AEMeasurable (X i) P) :
iIndepFun X P ↔
∀ L,
charFunDual (P.map (fun ω ↦ toLp p (X · ω))) L =
∏ i,
charFunDual (P.map (X i))
(L.comp ((PiLp.continuousLinearEquiv p ℝ E).symm.toContinuousLinearMap.comp (.single ℝ E i))) :=
by
rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff' p,
AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
