measurable_density_right — Mathlib

English

For fixed a ∈ α, the map x ↦ density κ ν a x s is measurable for any measurable s.

Русский

При фиксированном a плотность κ ν по x на s измерима.

LaTeX

$$Measurable (fun x => density κ ν a x s)$$

Lean4

theorem measurable_density_right (κ : Kernel α (γ × β)) (ν : Kernel α γ) {s : Set β} (hs : MeasurableSet s) (a : α) :
    Measurable (fun x ↦ density κ ν a x s) :=
  by
  change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun x ↦ (a, x)))
  exact (measurable_density κ ν hs).comp measurable_prodMk_left

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