measurable_kernel_prodMk_left — Mathlib

English

Let κ be an S-finite kernel κ: α → β. For every measurable set t ⊆ α × β, the map a ↦ κ(a)( { b ∈ β : (a,b) ∈ t } ) is measurable.

Русский

Пусть κ — сингрегулярное ядро κ: α → β. Для любого измеримого множества t ⊆ α × β отображение a ↦ κ(a){ b ∈ β | (a,b) ∈ t } является измеримым.

LaTeX

$$$\\text{Measurable}\\bigl( a \\mapsto \\kappa(a)(\\{ b \\in \\beta : (a,b) \\in t\\}) \\bigr)$$$

Lean4

theorem measurable_kernel_prodMk_left [IsSFiniteKernel κ] {t : Set (α × β)} (ht : MeasurableSet t) :
    Measurable fun a => κ a (Prod.mk a ⁻¹' t) :=
  by
  rw [← Kernel.kernel_sum_seq κ]
  have (a : _) : Kernel.sum (Kernel.seq κ) a (Prod.mk a ⁻¹' t) = ∑' n, Kernel.seq κ n a (Prod.mk a ⁻¹' t) :=
    Kernel.sum_apply' _ _ (measurable_prodMk_left ht)
  simp_rw [this]
  refine Measurable.ennreal_tsum fun n => ?_
  exact measurable_kernel_prodMk_left_of_finite ht inferInstance

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