English
Under the σ-finite assumption, the log of the RN-derivative of the tilted measure satisfies: log((μ.tilted f).rnDeriv μ x) = f(x) − log(∫ e^{f} dμ) almost everywhere w.r.t μ.
Русский
При предположении σ- конечности выполняется тождество: лог RN-дериватива наклонённой меры равен f(x) − log(∫ e^{f} dμ) почти наверняка по μ.
LaTeX
$$$\\log\\left((μ^{\\tilted f})\\mathrm{rnDeriv}_{μ}(x)^{\\toReal}\\right) =_{μ}^{\\mathrm{ae}} f(x) - \\log\\left(\\int e^{f} dμ\\right).$$$
Lean4
theorem log_rnDeriv_tilted_left_self [SigmaFinite μ] (hf : Integrable (fun x ↦ exp (f x)) μ) :
(fun x ↦ log ((μ.tilted f).rnDeriv μ x).toReal) =ᵐ[μ] fun x ↦ f x - log (∫ x, exp (f x) ∂μ) := by
cases eq_zero_or_neZero μ with
| inl h => simp_rw [h, ae_zero, Filter.EventuallyEq]; exact Filter.eventually_bot
| inr h0 =>
have hf' : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
filter_upwards [rnDeriv_tilted_left_self hf'] with x hx
rw [hx, ENNReal.toReal_ofReal (by positivity), log_div (exp_pos _).ne', log_exp]
exact (integral_exp_pos hf).ne'
