English
Under finiteness of μ and a bound on increments, limsup of a sequence of events s(n) is a.s. included in the limit of the conditional expectations, establishing Levy’s generalization for martingale parts.
Русский
При конечности μ и ограниченности приращений, limsup событий связаны с пределами условного ожидания, что формирует обобщение Леви для мартингальной части.
LaTeX
$$$$\forall^*\omega,\; \omega \in \limsup s\,\text{ atTop} \iff \displaystyle \lim_{n\to\infty} \sum_{k=0}^{n-1} \mathbb{E}[ (s(k+1)).indicator 1 \mid \mathcal{F}_k](\omega) = \infty.$$$$
Lean4
/-- Any `ℕ`-indexed stochastic process can be written as the sum of a martingale and a predictable
process. This is the predictable process. See `martingalePart` for the martingale. -/
noncomputable def predictablePart {m0 : MeasurableSpace Ω} (f : ℕ → Ω → E) (ℱ : Filtration ℕ m0) (μ : Measure Ω) :
ℕ → Ω → E := fun n => ∑ i ∈ Finset.range n, μ[f (i + 1) - f i|ℱ i]
