measurable_density_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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