English
Progressive measurability: a process u is ProgMeasurable with respect to f if, for every i, the restriction of u to Set.Iic i × Ω is measurable with respect to the product σ-algebra where Ω uses f i.
Русский
Прогрессивная измеримость: процесс u относительно фильтрации f таков, что на каждом уровне i отображение ограничено на Set.Iic i × Ω является измеримым.
LaTeX
$$$\\mathrm{ProgMeasurable}(f,u)$$$
Lean4
/-- Progressively measurable process. A sequence of functions `u` is said to be progressively
measurable with respect to a filtration `f` if at each point in time `i`, `u` restricted to
`Set.Iic i × Ω` is measurable with respect to the product `MeasurableSpace` structure where the
σ-algebra used for `Ω` is `f i`.
The usual definition uses the interval `[0,i]`, which we replace by `Set.Iic i`. We recover the
usual definition for index types `ℝ≥0` or `ℕ`. -/
def ProgMeasurable [MeasurableSpace ι] (f : Filtration ι m) (u : ι → Ω → β) : Prop :=
∀ i, StronglyMeasurable[Subtype.instMeasurableSpace.prod (f i)] fun p : Set.Iic i × Ω => u p.1 p.2
