stronglyMeasurable_countableFiltration_densityProcess

English

The densityProcess is strongly Measurable with respect to the countableFiltration γ n.

Русский

DensityProcess является сильно измеримой относительно countableFiltration γ n.

LaTeX

$$$\mathsf{StronglyMeasurable}\big( densityProcess(\kappa,\nu,n,\cdot) \big)$$$

Lean4

theorem stronglyMeasurable_countableFiltration_densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) (a : α)
    {s : Set β} (hs : MeasurableSet s) :
    StronglyMeasurable[countableFiltration γ n] (fun x ↦ densityProcess κ ν n a x s) :=
  (measurable_countableFiltration_densityProcess κ ν n a hs).stronglyMeasurable

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