exp_neg_llr' — Mathlib

English

If ν ≪ μ with sigma-finite measures, then ν-almost everywhere, exp(-llr(μ, ν)) equals (ν.rnDeriv μ).toReal.

Русский

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

LaTeX

$$$\\exp(-\\mathrm{llr}(\\mu, \\nu)(x)) = (\\nu\\!\\r nDeriv\\; \\mu)(x).toReal \\quad (\\text{ν-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, neg_eq_iff_eq_neg] at hx
  rw [← hx, hx_exp_log]

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