llr_self

Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

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

English

For any μ with Sigma-finiteness, llr μ μ is equal to 0 μ-a.e.

Русский

Для любой μ с суммарной конечной мерой llr μ μ равно 0 почти всюду относительно μ.

LaTeX

$$$llr(μ,μ)(x) = 0$ для μ-a.e. x.$$

Lean4

theorem llr_self (μ : Measure α) [SigmaFinite μ] : llr μ μ =ᵐ[μ] 0 := by
  filter_upwards [μ.rnDeriv_self] with a ha using by simp [llr, ha]

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

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

Разделы

Аффилиация

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