measurable_llr

Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measurable_llr

English

The log-likelihood ratio llr(μ, ν) is a measurable function of its argument.

Русский

Логарифмическое отношение правдоподобия llr(μ, ν) является измеримой функцией.

LaTeX

$$$\\text{Measurable}(\\llr\\;\\mu\\;\\nu)$$$

Lean4

@[measurability, fun_prop]
theorem measurable_llr (μ ν : Measure α) : Measurable (llr μ ν) :=
  (Measure.measurable_rnDeriv μ ν).ennreal_toReal.log

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

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

Разделы

Аффилиация

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