condIndepFun_self_right — Mathlib

English

Two random variables X and Z are conditionally independent with respect to σ(Z) (symmetric version).

Русский

Две случайные величины X и Z условно независимы относительно σ(Z) (симметричная версия).

LaTeX

$$$X \\perp_{\\sigma(Z)} Z$$$

Lean4

theorem condIndepFun_self_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {X : Ω → β} {Z : Ω → β'}
    (hX : Measurable X) (hZ : Measurable Z) : CondIndepFun (mβ'.comap Z) hZ.comap_le X Z μ :=
  condIndepFun_of_measurable_right hX (comap_measurable Z)

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