iIndepFun_iff_charFun_pi — Mathlib

English

From a family of sets s_i with indicator functions into a base monoid, the map is iIndepFun.

Русский

Из семейства множеств s_i с индикаторными функциями в базисный моноид отображение образуется как iIndepFun.

LaTeX

$$$iIndepFun\\big(\\lambda i, (s_i).indicator(1)\\big)\\mu$$$

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 the version for Hilbert
spaces, see `iIndepFun_iff_charFunDual_pi` for the Hilbert space version. -/
theorem iIndepFun_iff_charFun_pi (hX : ∀ i, AEMeasurable (X i) P) :
    iIndepFun X P ↔ ∀ t, charFun (P.map (fun ω ↦ toLp 2 (X · ω))) t = ∏ i, charFun (P.map (X i)) (t i) := by
  rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFun_eq_pi_iff,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

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