toKernel — Mathlib

English

For hf, the kernel produced by toKernel satisfies K(p) = (f p).measure.

Русский

Ядеро, полученное через toKernel, удовлетворяет K(p) = (f p).measure.

LaTeX

$$$\bigl(\text{IsCondKernelCDF.toKernel}(f, hf)\bigr)(p) = (f(p)).\text{measure}$.$$

Lean4

/-- A function `f : α × β → StieltjesFunction` with the property `IsCondKernelCDF f κ ν` gives a
Markov kernel from `α × β` to `ℝ`, by taking for each `p : α × β` the measure defined by `f p`. -/
noncomputable def toKernel (f : α × β → StieltjesFunction) (hf : IsCondKernelCDF f κ ν) : Kernel (α × β) ℝ
    where
  toFun p := (f p).measure
  measurable' := StieltjesFunction.measurable_measure hf.measurable hf.tendsto_atBot_zero hf.tendsto_atTop_one

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