condDistrib_self — Mathlib

English

If X is any map and c is a constant, condDistrib (const c) X μ is a.a. equal to the deterministic kernel assigning c.

Русский

Если X произвольна и константа c, condDistrib (константа c) X μ равняется детерминированному ядру, присваивающему c почти наверняка.

LaTeX

$$$$ \\mathrm{condDistrib}(\\text{const } c, X, μ) =_{a.e.} \\mathrm{deterministic}(c). $$$$

Lean4

theorem condDistrib_self (Y : α → Ω) : condDistrib Y Y μ =ᵐ[μ.map Y] Kernel.id := by
  simpa using condDistrib_comp_self Y measurable_id

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