condIndepFun_self_left — Mathlib

English

Two random variables X and Z are conditionally independent with respect to the σ-algebra generated by Z; i.e., X ⟂ Z | σ(Z).

Русский

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

LaTeX

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

Lean4

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

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