English
A finite kernel κ yields integrable real-valued kernels on measurable sets; for any measurable s, the function x ↦ (κ x).real s is integrable with respect to any finite measure μ.
Русский
Пусть κ — конечное ядро; тогда для каждого измеримого множества s функция x ↦ (κ x).real s интегрируема по мере μ, если μ конечна.
LaTeX
$$$\\int f \\, d(\\kappa x) \\; \\, \\text{real} \\, s \\, d\\mu < \\infty$ и т.д. (формально: Интеграл по μ от функции x ↦ (κ x).real s существует)$$
Lean4
theorem integrable (μ : Measure α) [IsFiniteMeasure μ] (κ : Kernel α β) [IsFiniteKernel κ] {s : Set β}
(hs : MeasurableSet s) : Integrable (fun x ↦ (κ x).real s) μ :=
by
refine
Integrable.mono' (integrable_const κ.bound.toReal) ((κ.measurable_coe hs).ennreal_toReal.aestronglyMeasurable)
(ae_of_all μ fun x ↦ ?_)
rw [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
exact ENNReal.toReal_mono (Kernel.bound_ne_top _) (Kernel.measure_le_bound _ _ _)
