measurable_klFun

Mathlib.InformationTheory.KullbackLeibler.KLFun

URI: https://scilib.ai/kg/mathlib#InformationTheory.measurable_klFun

English

The function klFun is measurable with respect to the Borel sigma-algebra on the reals.

Русский

Функция klFun измерима относительно борелевской сигма-алгебры чисел.

LaTeX

$$$\\mathrm{Measurable}(\\mathrm{klFun})$$$

Lean4

/-- `klFun` is measurable. -/
@[measurability, fun_prop]
theorem measurable_klFun : Measurable klFun :=
  continuous_klFun.measurable

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

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

Разделы

Аффилиация

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