progMeasurable_const — Mathlib

English

A constant process b is progressively measurable with respect to any filtration f.

Русский

Постоянный процесс b является прогрессивно измеримым относительно любой фильтрации f.

LaTeX

$$$\\mathrm{ProgMeasurable}(f, (\\lambda\\_i\\,\\omega.\\, b))$$$

Lean4

theorem progMeasurable_const [MeasurableSpace ι] (f : Filtration ι m) (b : β) :
    ProgMeasurable f (fun _ _ => b : ι → Ω → β) := fun i =>
  @stronglyMeasurable_const _ _ (Subtype.instMeasurableSpace.prod (f i)) _ _

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