measurable_countableFiltration_densityProcess

English

The densityProcess is measurable with respect to the filtration countableFiltration γ n, for fixed a and s measurable.

Русский

DensityProcess измеримо относительно фильтрации countableFiltration γ n при фиксированных a и измеримом s.

LaTeX

$$$\mathsf{Measurable}_{countableFiltration\;\gamma\;n}\left( p \mapsto \text{densityProcess}(\kappa,\nu,n,p.1,p.2,s) \right)$$$

Lean4

theorem measurable_countableFiltration_densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) (a : α)
    {s : Set β} (hs : MeasurableSet s) : Measurable[countableFiltration γ n] (fun x ↦ densityProcess κ ν n a x s) :=
  by
  refine @Measurable.ennreal_toReal _ (countableFiltration γ n) _ ?_
  exact (measurable_densityProcess_countableFiltration_aux κ ν n hs).comp measurable_prodMk_left

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