English
Exp of llr is μ-ae equal to a piecewise expression: exp(llr μ ν x) = 1 if μ.rnDeriv ν x = 0, else (μ.rnDeriv ν x).toReal.
Русский
Экспонента от llr равна единице там, где rnDeriv равен нулю, иначе равно toReal rnDeriv.
LaTeX
$$$\\exp(llr(μ,ν)(x)) = 1\\ \\text{ if } μ.rnDeriv ν x = 0, \\text{ иначе } (μ.rnDeriv ν x).toReal$ (μ-a.e.).$$
Lean4
theorem exp_llr (μ ν : Measure α) [SigmaFinite μ] :
(fun x ↦ exp (llr μ ν x)) =ᵐ[ν] fun x ↦ if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal :=
by
filter_upwards [Measure.rnDeriv_lt_top μ ν] with x hx
by_cases h_zero : μ.rnDeriv ν x = 0
· simp only [llr, h_zero, ENNReal.toReal_zero, log_zero, exp_zero, ite_true]
· rw [llr, exp_log, if_neg h_zero]
exact ENNReal.toReal_pos h_zero hx.ne
