condExpKernel_def — Mathlib

English

Conditional expectation of f under condDistrib with id mapping equals the integral of f against condDistrib id X μ.

Русский

Условное ожидание f при condDistrib id эквивалентно интегралу по condDistrib id X μ.

LaTeX

$$$$ \\mu[f|mβ.comap X] =^{}_{μ} \\int_y f(y) \\; d(\\operatorname{condDistrib}(id,X,μ))(y). $$$$

Lean4

theorem condExpKernel_def : eta_helper Eq✝ @condExpKernel.{} @(delta% @definition✝) :=
  by
  intros
  delta condExpKernel
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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