integrable_llr_tilted_right — Mathlib

English

Under finite μ and sigma-finite ν, with integrability of f and llr, the tilted llr μ (ν.tilted f) is μ-integrable.

Русский

При конечной μ и сигма-ограниченной ν, и интегрируемости f и llr, llr(μ, ν.tilted f) интегрируема по μ.

LaTeX

$$$\\text{Integrable}(\\mathrm{llr}(\\mu, \\nu\\tilted f))_{\\mu}$$$

Lean4

theorem integrable_llr_tilted_right [IsFiniteMeasure μ] [SigmaFinite ν] (hμν : μ ≪ ν) (hfμ : Integrable f μ)
    (h_int : Integrable (llr μ ν) μ) (hfν : Integrable (fun x ↦ exp (f x)) ν) : Integrable (llr μ (ν.tilted f)) μ :=
  by
  rw [integrable_congr (llr_tilted_right hμν hfν)]
  exact Integrable.add (hfμ.neg.add (integrable_const _)) h_int

Похожие утверждения