martingale_densityProcess — Mathlib

English

The martingale property holds for the densityProcess across the filtration sequence.

Русский

Свойство мартингала справедливо для densityProcess по последовательности фильтраций.

LaTeX

$$$\text{Martingale}\big( \text{densityProcess}, \text{countableFiltration} \gamma \big)$$$

Lean4

theorem martingale_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    Martingale (fun n x ↦ densityProcess κ ν n a x s) (countableFiltration γ) (ν a) :=
  ⟨adapted_densityProcess κ ν a hs, fun _ _ h ↦ condExp_densityProcess hκν h a hs⟩

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