English
Equality holds between the martingalePart and predicted minus the process; i.e., predictable part is the remainder after subtracting the martingale part from f.
Русский
Существует равенство между martingalePart и остающейся частью: предсказуемая часть равна f минус мартингальная часть.
LaTeX
$$$$\mathrm{martingalePart}(f, \mathcal{F}, \mu)(n,\omega) = f(n,\omega) - \mathrm{predictablePart}(f, \mathcal{F}, \mu)(n,\omega).$$$$
Lean4
/-- Any `ℕ`-indexed stochastic process can be written as the sum of a martingale and a predictable
process. This is the martingale. See `predictablePart` for the predictable process. -/
noncomputable def martingalePart {m0 : MeasurableSpace Ω} (f : ℕ → Ω → E) (ℱ : Filtration ℕ m0) (μ : Measure Ω) :
ℕ → Ω → E := fun n => f n - predictablePart f ℱ μ n
