measurable_kernel_prodMk_left' — Mathlib

English

For an S-finite kernel η on (α × β) → γ and a measurable s ⊆ β × γ, the map a ↦ η(a,·)(Prod.mk · ⁻¹' s) is Measurable in the second argument for every fixed a.

Русский

Для ядра η на (α × β) → γ и измеримого множества s ⊆ β × γ отображение a ↦ η(a, b)(Prod.mk b ⁻¹' s) измеримо по b для каждого фиксированного a.

LaTeX

$$$\\forall a,\\; \\text{Measurable}\\bigl(b \\mapsto \\eta(a,b)(\\{ c : (b,c) \\in s \\})\\bigr)$$$

Lean4

theorem measurable_kernel_prodMk_left' [IsSFiniteKernel η] {s : Set (β × γ)} (hs : MeasurableSet s) (a : α) :
    Measurable fun b => η (a, b) (Prod.mk b ⁻¹' s) :=
  by
  have (b : _) : Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p : (α × β) × γ | (p.1.2, p.2) ∈ s}} := rfl
  simp_rw [this]
  refine (measurable_kernel_prodMk_left ?_).comp measurable_prodMk_left
  exact (measurable_fst.snd.prodMk measurable_snd) hs

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