exp_neg_llr — Mathlib

English

Suppose μ ≪ ν with sigma-finite measures. Then almost everywhere with respect to μ, exp(-llr(μ, ν)(x)) equals the real-valued Radon-Nikodym derivative of ν with respect to μ at x: (ν.rnDeriv μ)(x).toReal.

Русский

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

LaTeX

$$$\\exp(-\\mathrm{llr}(\\mu, \\nu)(x)) = (\\nu\\!\\downarrow\\!\\mathrm{rnDeriv}\\; \\mu)(x).toReal \\quad \\text{for μ-a.e. } x$$$

Lean4

theorem exp_neg_llr [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    (fun x ↦ exp (-llr μ ν x)) =ᵐ[μ] fun x ↦ (ν.rnDeriv μ x).toReal :=
  by
  filter_upwards [neg_llr hμν, exp_llr_of_ac' ν μ hμν] with x hx hx_exp_log
  rw [Pi.neg_apply] at hx
  rw [hx, hx_exp_log]

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