iIndepFun_iff_charFunDual_pi — Mathlib

English

Same as above with AEMeasurability: independence of the Finset product not containing a given index.

Русский

То же самое в случае AEMeasurability: независимость произведения по конечному подмножеству не содержащему индекс.

LaTeX

$$$\\forall s,i, i \\notin s \\Rightarrow IndepFun(\\prod_{j\\in s} f_j, f_i)\\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 Banach
spaces, 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 ω ↦ (X · ω))) L = ∏ i, charFunDual (P.map (X i)) (L.comp (.single ℝ E i)) :=
  by rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff]

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