condExpKernel_eq — Mathlib

English

The conditional expectation kernel equals the comap of the conditional distribution by the identity map, in a particular sigma-algebra arrangement.

Русский

Условное ядро ожидания равно отображению обратного образа условного распределения по тождественному отображению в заданной задаче сигма-алгебр.

LaTeX

$$$\\operatorname{condExpKernel}(\\mu, m) = \\operatorname{comap}(\\operatorname{condDistrib}(id,id,\\mu))\\; id$$$

Lean4

theorem condExpKernel_eq (μ : Measure Ω) [IsFiniteMeasure μ] [h : Nonempty Ω] (m : MeasurableSpace Ω) :
    condExpKernel (mΩ := mΩ) μ m =
      Kernel.comap (@condDistrib Ω Ω Ω mΩ _ _ mΩ (m ⊓ mΩ) id id μ _) id (measurable_id'' (inf_le_left : m ⊓ mΩ ≤ m)) :=
  by simp [condExpKernel, h]

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