toKernel_apply

Mathlib.Probability.Kernel.Disintegration.CDFToKernel

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.IsCondKernelCDF.toKernel_apply

English

Equality holds: the application of toKernel to f hf equals the measure-valued function (f p).measure.

Русский

Равенство: применение toKernel к f hf равно функции меры (f p).measure.

LaTeX

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

Lean4

theorem toKernel_apply {hf : IsCondKernelCDF f κ ν} (p : α × β) : hf.toKernel f p = (f p).measure :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru