measurable_densityProcess_aux — Mathlib

English

For fixed κ, ν, n, x, the map a ↦ densityProcess κ ν n a x s is measurable.

Русский

Для фиксированных κ, ν, n, x отображение a ↦ densityProcess κ ν n a x s измеримо.

LaTeX

$$$\mathsf{Measurable}\big( a \mapsto \text{densityProcess}(\kappa,\nu,n,a,x,s) \big)$$$

Lean4

theorem measurable_densityProcess_aux (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) {s : Set β}
    (hs : MeasurableSet s) :
    Measurable (fun (p : α × γ) ↦ κ p.1 (countablePartitionSet n p.2 ×ˢ s) / ν p.1 (countablePartitionSet n p.2)) :=
  by
  refine Measurable.mono (measurable_densityProcess_countableFiltration_aux κ ν n hs) ?_ le_rfl
  exact sup_le_sup le_rfl (comap_mono ((countableFiltration γ).le _))

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