integral_densityProcess — Mathlib

English

The condExp of the densityProcess across i,j equals the densityProcess at i with respect to the filtration just before i, almost surely.

Русский

Условное ожидание densityProcess по i,j равно densityProcess при i относительно предшествующей фильтрации, почти наверняка.

LaTeX

$$$\text{condExpDensityProcess}(\kappa,\nu,i,j) = \text{densityProcess}(\kappa,\nu,i,\cdot,\cdot)$ a.e.$$

Lean4

theorem integral_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β}
    (hs : MeasurableSet s) : ∫ x, densityProcess κ ν n a x s ∂(ν a) = (κ a).real (univ ×ˢ s) := by
  rw [← setIntegral_univ, setIntegral_densityProcess hκν _ _ hs MeasurableSet.univ]

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