condIndepFun_of_measurable_right — Mathlib

English

Let X: Ω → β be measurable and Y: Ω → β' be m'-measurable. Then X and Y are conditionally independent given m' (with respect to μ).

Русский

Пусть X: Ω → β измерима, а Y: Ω → β' измерима в отношении m'. Тогда X и Y условно независимы относительно m' по μ.

LaTeX

$$$X \\perp_{m'} Y$$$

Lean4

theorem condIndepFun_of_measurable_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {X : Ω → β} {Y : Ω → β'}
    (hX : Measurable X) (hY : Measurable[m'] Y) : CondIndepFun m' hm' X Y μ :=
  (condIndepFun_of_measurable_left hY hX).symm

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