exp_llr_of_ac' — Mathlib

English

llr μ ν x equals log( rnDeriv ν x ) when comparing measures.

Русский

llr μ ν x равно log( rnDeriv ν x ) при сравнении мер.

LaTeX

$$$llr(μ,ν)(x) = \\log(μ.rnDeriv ν x).toReal$$$

Lean4

theorem exp_llr_of_ac' (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] (hμν : ν ≪ μ) :
    (fun x ↦ exp (llr μ ν x)) =ᵐ[ν] fun x ↦ (μ.rnDeriv ν x).toReal :=
  by
  filter_upwards [exp_llr μ ν, Measure.rnDeriv_pos' hμν] with x hx hx_pos
  rwa [if_neg hx_pos.ne'] at hx

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