instIsMarkovKernel_toKernel — Mathlib

English

If f, κ, ν form a conditional-CDF structure IsCondKernelCDF, then the derived kernel hf.toKernel f is a Markov kernel.

Русский

Если f, κ, ν образуют структуру условной распределительной функции (CDF), и выполнено IsCondKernelCDF, то полученное ядро hf.toKernel f является марковским ядром.

LaTeX

$$$IsMarkovKernel\left(hf.toKernel f\right)$$$

Lean4

instance instIsMarkovKernel_toKernel {hf : IsCondKernelCDF f κ ν} : IsMarkovKernel (hf.toKernel f) :=
  ⟨fun _ ↦ (f _).isProbabilityMeasure (hf.tendsto_atBot_zero _) (hf.tendsto_atTop_one _)⟩

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