integrable_density — Mathlib

English

For any a and s with measurable s, the function x ↦ density κ ν a x s is integrable with respect to ν a.

Русский

Для любого a и измеримого s функция x ↦ density κ ν a x s интегрируема по мере ν a.

LaTeX

$$Integrable (fun x => density κ ν a x s) (ν a)$$

Lean4

theorem integrable_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    Integrable (fun x ↦ density κ ν a x s) (ν a) :=
  by
  rw [← memLp_one_iff_integrable]
  refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩
  · exact measurable_density_right κ ν hs a
  · exact (eLpNorm_density_le hκν a s).trans_lt (measure_lt_top _ _)

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