English
As above, but with the RN-derivative taken to real numbers: the a.e. equality for the real-valued RN-derivative of the left tilt is exp(f) / ∫ exp(f) dμ times the real RN-derivative of ν with respect to μ.
Русский
Как и выше, но для вещественного RN-дериватива левого наклона: почти наверняка верно равенство exp(f) / ∫ exp(f) dμ умноженное на вещественный RN-дериватив ν по отношению к μ.
LaTeX
$$$(μ^{\\tilted f})\\mathrm{rnDeriv}_{ν}(x)^{\\toReal} =_{ν}^{\\mathrm{ae}} \\dfrac{e^{f(x)}}{\\int e^{f} dμ} \\cdot (μ\\mathrm rnDeriv_{ν}(x))^{\\toReal}.$$$
Lean4
theorem toReal_rnDeriv_tilted_left {ν : Measure α} [SigmaFinite μ] [SigmaFinite ν] (hfν : AEMeasurable f ν) :
(fun x ↦ ((μ.tilted f).rnDeriv ν x).toReal) =ᵐ[ν] fun x ↦
exp (f x) / (∫ x, exp (f x) ∂μ) * (μ.rnDeriv ν x).toReal :=
by
filter_upwards [rnDeriv_tilted_left μ 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)
