exp_llr_of_ac — Mathlib

English

If ν is absolutely continuous w.r.t μ, then exp(llr μ ν) equals (μ.rnDeriv ν) a.e. with ν.

Русский

Если ν абсолютно непрерывна относительно μ, то exp(llr μ ν) равняется rnDeriv ν μ почти всюду по ν.

LaTeX

$$$\\forall \\text{a.e. } x,\\; \\exp(llr(μ,ν)(x)) = (μ.rnDeriv ν x).toReal$ (ν-a.e.).$$

Lean4

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

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