English
For a sigma-finite μ and ν, and a measurable function f with certain integrability properties, the llr for the tilted measure μ.tilted f against ν equals f−log(∫ e^{f} dμ) + llr(μ, ν) a.e.μ.
Русский
При сигма-ограниченных μ и ν и измеримой функции f, llr для сдвинутой меры μ.tilted f против ν равен f−log(∫ e^{f} dμ) + llr(μ, ν) почти всюду по μ.
LaTeX
$$$\\mathrm{llr}(\\mu\\mathrel{.\\!\\text{tilted}} f, \\nu) =_{\\mu\\text{-a.e.}} f - \\log\\left(\\int e^{f} \\mathrm{d}\\mu\\right) + \\mathrm{llr}(\\mu, \\nu)$$$
Lean4
theorem llr_tilted_left [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (hf : Integrable (fun x ↦ exp (f x)) μ)
(hfν : AEMeasurable f ν) : (llr (μ.tilted f) ν) =ᵐ[μ] fun x ↦ f x - log (∫ z, exp (f z) ∂μ) + llr μ ν x := by
cases eq_zero_or_neZero μ with
| inl hμ => simp only [hμ, ae_zero, Filter.EventuallyEq, Filter.eventually_bot]
| inr
h0 =>
filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_left μ 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, div_eq_mul_inv, log_mul (exp_pos _).ne', log_exp, log_inv, llr, ← sub_eq_add_neg]
· simp only [ne_eq, inv_eq_zero]
exact (integral_exp_pos hf).ne'
· simp only [ne_eq, div_eq_zero_iff]
push_neg
exact ⟨(exp_pos _).ne', (integral_exp_pos hf).ne'⟩
· simp [ENNReal.toReal_eq_zero_iff, hx_lt_top.ne, hx_pos.ne']
