integrable_kernel_prodMk_left — Mathlib

English

A variant of the universal bound using the same structure, showing the same inequality in a different presentation.

Русский

Вариант неравенства с тем же худым построением.

LaTeX

$$$$ (κ ⊗ₖ η) a \\ Set.univ \\le κ a \\ Set.univ \\cdot η.bound. $$$$

Lean4

theorem integrable_kernel_prodMk_left (a : α) {s : Set (β × γ)} (hs : MeasurableSet s) (h2s : (κ ⊗ₖ η) a s ≠ ∞) :
    Integrable (fun b => (η (a, b)).real (Prod.mk b ⁻¹' s)) (κ a) :=
  by
  constructor
  · exact (measurable_kernel_prodMk_left' hs a).ennreal_toReal.aestronglyMeasurable
  · exact hasFiniteIntegral_prodMk_left a h2s

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