llr — Mathlib

English

The log-likelihood ratio llr(μ,ν, x) is defined as log((rnDeriv ν x)↑).toReal, i.e., the log of the Radon–Nikodym derivative of ν with respect to μ at x.

Русский

Логарифм отношения правдоподобия llr(μ,ν, x) задаётся как log( rnDeriv ν x ) в реальном числе.

LaTeX

$$$\\mathrm{llr}(μ,ν)(x) = \\log((μ.rnDeriv ν x))^{\\mathrm{toReal}}$$$

Lean4

/-- Log-Likelihood Ratio between two measures. -/
noncomputable def llr (μ ν : Measure α) (x : α) : ℝ :=
  log (μ.rnDeriv ν x).toReal

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