setIntegral_densityProcess_of_le — Mathlib

English

The densityProcess forms a martingale as stated, combining adaptedness and condExp equality.

Русский

DensityProcess образует мартингал, объединяющий адаптированность и равенство condExp.

LaTeX

$$$\text{Martingale}\big( (n,a) \mapsto \text{densityProcess}(\kappa,\nu,n,a,\cdot,\cdot), \text{countableFiltration} \gamma \big)$$$

Lean4

theorem setIntegral_densityProcess_of_le (hκν : fst κ ≤ ν) [IsFiniteKernel ν] {n m : ℕ} (hnm : n ≤ m) (a : α)
    {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet[countableFiltration γ n] A) :
    ∫ x in A, densityProcess κ ν m a x s ∂(ν a) = (κ a).real (A ×ˢ s) :=
  setIntegral_densityProcess hκν m a hs ((countableFiltration γ).mono hnm A hA)

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