English
For sigma-finite μ and ν, and integrable exp(f) with respect to ν, the tilted llr μ (ν.tilted f) equals -f + log(∫ e^{f} dν) + llr μ ν a.e.μ.
Русский
При σ-ограниченных μ и ν и интегрируемости exp(f) по ν., llr(μ, ν.tilted f) равно -f + log(∫ e^{f}) + llr(μ, ν) почти всюду по μ.
LaTeX
$$$\\mathrm{llr}(\\mu, \\nu\\tilted f) =_{\\mu\\text{-a.e.}} -f + \\log\\left(\\int e^{f} \\, d\\nu\\right) + \\mathrm{llr}(\\mu, \\nu)$$$
Lean4
theorem llr_tilted_right [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (hf : Integrable (fun x ↦ exp (f x)) ν) :
(llr μ (ν.tilted f)) =ᵐ[μ] fun x ↦ -f x + log (∫ z, exp (f z) ∂ν) + llr μ ν x := by
cases eq_zero_or_neZero ν with
| inl h =>
have hμ : μ = 0 := by ext s _; exact hμν (by simp [h])
simp only [hμ, ae_zero, Filter.EventuallyEq, Filter.eventually_bot]
| inr
h0 =>
filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_right μ ν hf), Measure.rnDeriv_pos hμν,
hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx hx_pos hx_lt_top
rw [llr, hx, log_mul, log_mul (exp_pos _).ne', log_exp, llr]
· exact (integral_exp_pos hf).ne'
· refine (mul_pos (exp_pos _) (integral_exp_pos hf)).ne'
· simp [ENNReal.toReal_eq_zero_iff, hx_lt_top.ne, hx_pos.ne']
