condExpKernel_comp_trim — Mathlib

English

For hm with m ≤ mΩ, condExpKernel μ m composed with μ.trim hm recovers μ.

Русский

При hm с m ≤ mΩ ядро condExpKernel μ m, затем применение μ.trim hm возвращает μ.

LaTeX

$$$\\text{condExpKernel}(\\mu,m)\\circ\\mu\\text{.trim}(hm)=\\mu$$$

Lean4

theorem condExpKernel_comp_trim (hm : m ≤ mΩ) : condExpKernel μ m ∘ₘ μ.trim hm = μ :=
  by
  rw [← Measure.snd_compProd, compProd_trim_condExpKernel, @Measure.snd_map_prodMk, Measure.map_id]
  exact measurable_id'' hm

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