adapted_densityProcess — Mathlib

English

The densityProcess is adapted to the filtration countableFiltration γ, i.e., for each fixed a, the mapping n ↦ densityProcess κ ν n a · s is adapted.

Русский

DensityProcess адаптирован к фильтрации countableFiltration γ, то есть отображение n ↦ densityProcess κ ν n a · s является адаптированным.

LaTeX

$$$\mathsf{Adapted}\big( countableFiltration\;\gamma \;\, ,\; (n,x) \mapsto \text{densityProcess}(\kappa,\nu,n,a,x,s) \big)$$$

Lean4

theorem adapted_densityProcess (κ : Kernel α (γ × β)) (ν : Kernel α γ) (a : α) {s : Set β} (hs : MeasurableSet s) :
    Adapted (countableFiltration γ) (fun n x ↦ densityProcess κ ν n a x s) := fun n ↦
  stronglyMeasurable_countableFiltration_densityProcess κ ν n a hs

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