measurable_lintegral_indicator_const

English

Let κ be an S-finite kernel. For a measurable set s ⊆ β × α, the map y ↦ κ(y)( (f x)⁻¹' s ) is measurable, where f maps x ↦ (x,y).

Русский

Пусть κ — S‑конечное ядро. Для измеримого набора s ⊆ β × α отображение y ↦ κ(y)((x,y)⁻¹' s) измеримо, где x зависит от y через соответствующее отображение.

LaTeX

$$$\\text{Measurable}\\bigl(y \\mapsto \\kappa(y)((\\mathrm{fun}\\ x \\mapsto (x,y))^{-1}'s)\\bigr)$$$

Lean4

/-- Auxiliary lemma for `Measurable.lintegral_kernel_prod_right`. -/
theorem measurable_lintegral_indicator_const {t : Set (α × β)} (ht : MeasurableSet t) (c : ℝ≥0∞) :
    Measurable fun a => ∫⁻ b, t.indicator (Function.const (α × β) c) (a, b) ∂κ a :=
  by
  unfold Function.const
  simp_rw [lintegral_indicator_const_comp measurable_prodMk_left ht _]
  exact Measurable.const_mul (measurable_kernel_prodMk_left ht) c

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