English
Assume μ ≪ ν with μ finite and ν σ-finite. If f is integrable with respect to μ, llr with respect to μ and ν is integrable, and exp(f) is ν-ae-measurable, then llr for the tilted μ by f against ν is μ-integrable.
Русский
Пусть μ ≪ ν, μ конечна, ν σ-конечна. Пусть f интегрируема по μ, llr μ ν интегрируема по μ и exp(f) ν-ae-measurable. Тогда llr(μ.tilted f, ν) интегрируема по μ.
LaTeX
$$$\\text{Integrable}(\\mathrm{llr}(\\mu, \\nu))_{\\mu} \\Rightarrow \\text{Integrable}(\\mathrm{llr}(\\mu\\tilted f, \\nu))_{\\mu}$$$
Lean4
theorem integrable_llr_tilted_left [IsFiniteMeasure μ] [SigmaFinite ν] (hμν : μ ≪ ν) (hf : Integrable f μ)
(h_int : Integrable (llr μ ν) μ) (hfμ : Integrable (fun x ↦ exp (f x)) μ) (hfν : AEMeasurable f ν) :
Integrable (llr (μ.tilted f) ν) μ :=
by
rw [integrable_congr (llr_tilted_left hμν hfμ hfν)]
exact Integrable.add (hf.sub (integrable_const _)) h_int
