English
Under the same hypotheses as above, the real-valued version of the RN-derivative equality holds: the a.e. equality of the real parts is given by the real-valued expression exp(-f) · ∫ exp(f) dν times the real part of μ.rnDeriv ν.
Русский
При тех же предположениях выполняется та же тождественность для вещественных значений RN-дериватива: почти везде при ν выполняется exp(-f) · ∫ exp(f) dν умноженное на (μ.rnDeriv ν) и затем приведённое к действительным значениям.
LaTeX
$$$\\big(\\mu\\mathrm{rnDeriv}(\\nu^{\\tilde f})(x)\\big)^{\\toReal} =_{\\nu}^{\\mathrm{ae}} e^{-f(x)}\\left(\\int e^{f} d\\nu\\right)\\cdot (\\mu\\mathrm rnDeriv_{\\nu}(x))^{\\toReal}.$$$
Lean4
theorem toReal_rnDeriv_tilted_right (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
(hf : Integrable (fun x ↦ exp (f x)) ν) :
(fun x ↦ (μ.rnDeriv (ν.tilted f) x).toReal) =ᵐ[ν] fun x ↦
exp (-f x) * (∫ x, exp (f x) ∂ν) * (μ.rnDeriv ν x).toReal :=
by
filter_upwards [rnDeriv_tilted_right μ ν hf] with x hx
rw [hx]
simp only [ENNReal.toReal_mul, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]
exact Or.inl (by positivity)
