measurable_density — Mathlib

English

For any fixed kernels κ and ν, the function (a, x) ↦ density κ ν a x s is measurable for any fixed measurable set s.

Русский

Для любых ядер κ и ν функция (a, x) ↦ density κ ν a x s измерима по a и x при фиксированном измеримом множестве s.

LaTeX

$$Measurable (fun (p : α × γ) ↦ density κ ν p.1 p.2 s)$$

Lean4

theorem measurable_density (κ : Kernel α (γ × β)) (ν : Kernel α γ) {s : Set β} (hs : MeasurableSet s) :
    Measurable (fun (p : α × γ) ↦ density κ ν p.1 p.2 s) :=
  .limsup (fun n ↦ measurable_densityProcess κ ν n hs)

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