indepFun_iff_charFunDual_prod' — Mathlib

English

AEMeasurable analogue of the sequential product independence: the product up to n is independent of the nth variable.

Русский

ААМеасурабельный аналог последовательной независимости: произведение до n независимо от n-го элемента.

LaTeX

$$$\\forall n, IndepFun\\Big(\\prod_{j

Lean4

/-- Two random variables are independent if and only if their joint characteristic function is equal
to the product of the characteristic functions. This is `indepFun_iff_charFunDual_prod` for
`WithLp`. See `indepFun_iff_charFun_prod` for the Hilbert space version. -/
theorem indepFun_iff_charFunDual_prod' (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
    IndepFun X Y P ↔
      ∀ L,
        charFunDual (P.map (fun ω ↦ toLp p (X ω, Y ω))) L =
          charFunDual (P.map X)
              (L.comp ((prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp (.inl ℝ E F))) *
            charFunDual (P.map Y)
              (L.comp ((prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp (.inr ℝ E F))) :=
  by
  rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff' p,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

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