English
Let μ be a measure and f: α → ℝ such that f is integrable under ν, then the RN-derivative of ν with respect to the tilted μ by f is ENNReal.ofReal(exp(f) / ∫ exp(f) dμ) times μ.rnDeriv ν a.e.
Русский
Пусть μ — мера и f: α → ℝ так, что f интегрируема по ν. Тогда RN-дериватив ν по отношению к наклонённой μ по f равен ENNReal.ofReal(exp(f)/(∫ exp(f) dμ)) умноженное на μ.rnDeriv ν почти наверняка.
LaTeX
$$$(μ^{\\tilted f})\\mathrm{rnDeriv}_{ν} =_{ν}^{\\mathrm{ae}} x \\mapsto \\mathrm{ENNReal.ofReal}\\left(\\frac{e^{f(x)}}{\\int e^{f} dμ}\\right) \\cdot (μ\\mathrm rnDeriv_{ν})(x).$$$
Lean4
theorem rnDeriv_tilted_left {ν : Measure α} [SigmaFinite μ] [SigmaFinite ν] (hfν : AEMeasurable f ν) :
(μ.tilted f).rnDeriv ν =ᵐ[ν] fun x ↦ ENNReal.ofReal (exp (f x) / (∫ x, exp (f x) ∂μ)) * μ.rnDeriv ν x :=
by
let g := fun x ↦ ENNReal.ofReal (exp (f x) / (∫ x, exp (f x) ∂μ))
refine Measure.rnDeriv_withDensity_left (μ := μ) (ν := ν) (f := g) ?_ ?_
· exact ((measurable_exp.comp_aemeasurable hfν).div_const _).ennreal_ofReal
· exact ae_of_all _ (fun x ↦ by simp [g])
