English
Under finite μ and sigma-finite ν, with hμν: μ ≪ ν and appropriate integrability of f and llr, the tilted llr is μ-integrable.
Русский
При конечной μ и сигма-ограниченной ν, и при выполнении условий на f и llr, llr(μ, ν) для сдвинутой меры интегрируема по μ.
LaTeX
$$$\\text{Integrable}(\\mathrm{llr}(\\mu, \\nu))_{\\mu} \\Rightarrow \\text{Integrable}(\\mathrm{llr}(\\mu, \\nu\\tilted f))_{\\mu}$$$
Lean4
theorem integral_llr_tilted_left [IsProbabilityMeasure μ] [SigmaFinite ν] (hμν : μ ≪ ν) (hf : Integrable f μ)
(h_int : Integrable (llr μ ν) μ) (hfμ : Integrable (fun x ↦ exp (f x)) μ) (hfν : AEMeasurable f ν) :
∫ x, llr (μ.tilted f) ν x ∂μ = ∫ x, llr μ ν x ∂μ + ∫ x, f x ∂μ - log (∫ x, exp (f x) ∂μ) := by
calc
∫ x, llr (μ.tilted f) ν x ∂μ = ∫ x, f x - log (∫ x, exp (f x) ∂μ) + llr μ ν x ∂μ :=
integral_congr_ae (llr_tilted_left hμν hfμ hfν)
_ = ∫ x, f x ∂μ - log (∫ x, exp (f x) ∂μ) + ∫ x, llr μ ν x ∂μ :=
by
rw [integral_add ?_ h_int]
swap; · exact hf.sub (integrable_const _)
rw [integral_sub hf (integrable_const _)]
simp only [integral_const, measureReal_univ_eq_one, smul_eq_mul, one_mul]
_ = ∫ x, llr μ ν x ∂μ + ∫ x, f x ∂μ - log (∫ x, exp (f x) ∂μ) := by abel
