neg_llr — Mathlib

English

Let μ and ν be sigma-finite measures with μ absolutely continuous with respect to ν. Then for μ-almost every x, the negative log-likelihood ratio equals the log-likelihood ratio with the roles of μ and ν reversed: -llr(μ, ν)(x) = llr(ν, μ)(x).

Русский

Пусть μ и ν — σ-конечные меры и μ абсолютно непрерывна по ν. Тогда почти всюду при μ выполняется равенство: -llr(μ, ν)(x) = llr(ν, μ)(x).

LaTeX

$$$-\\mathrm{llr}(\\mu, \\nu) =_{\\mu\\text{-a.e.}} \\mathrm{llr}(\\nu, \\mu)$$$

Lean4

theorem neg_llr [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) : -llr μ ν =ᵐ[μ] llr ν μ :=
  by
  filter_upwards [Measure.inv_rnDeriv hμν] with x hx
  rw [Pi.neg_apply, llr, llr, ← log_inv, ← ENNReal.toReal_inv]
  congr

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