Formalization of a Brownian motion and of stochastic integrals in Lean

11 Modifications with cadlag paths

11.1 Preliminaries

TODO: define cadlag.

11.2 Cadlag modifications of martingales

11.2.1 Upcrossings

Let \(X : T \to \Omega \to \mathbb {R}\) be a stochastic process on a finite time domain \(T\). Then for all \(a {\lt} b\) in \(\mathbb {R}\) and \(t \in T\), there exists an elementary predictable set \(A\) such that the number of upcrossings \(U_t[a, b]\) of the interval \([a, b]\) before time \(t\) satisfies

\begin{align*} (b - a) U_t[a, b] \le (\mathbb {1}_A \bullet X)_t + \max \{ a - X_t, 0\} \: . \end{align*}
Proof

See this chapter of [ .

In the proof, note that \(A\) can be written as a finite disjoint union of sets of the form \(\{ (t, \omega ) \mid \sigma (\omega ) {\lt} t \le \tau (\omega )\} \) for stopping times \(\sigma , \tau \). To see that each is an elementary predictable set, note that if \(T = \{ t_0, \ldots , t_n\} \) where \(t_0 {\lt} \cdots {\lt} t_n\), then it can be written as a finite disjoint union of sets

\begin{align*} \{ \sigma (\omega ) {\lt} t \le \tau (\omega )\} & = \bigcup _{k=1}^{n} {t_k} \times \{ \sigma {\lt} t_k \le \tau \} \\ & = \bigcup _{k=1}^{n} (t_{k-1}, t_k] \times \{ \sigma \le t_{k-1} {\lt} \tau \} \end{align*}

where \(\{ \sigma \le t_{k-1} {\lt} \tau \} \in \mathcal{F}_{t_{k-1}}\). Therefore \(A\) is an elementary predictable set.

11.2.2 Cadlag modifications

Let \(X : T \to \Omega \to \mathbb {R}\) be an adapted stochastic process such that one of the two following conditions hold:

  1. \(X\) is integrable and for every \(t \in T\) the set \(\{ \mathbb {E}[(\mathbb {1}_A \bullet X)_t] \mid A \text{ elementary predictable}\} \) is bounded.

  2. For every \(t \in T\) the set \(\{ (\mathbb {1}_A \bullet X)_t \mid A \text{ elementary predictable}\} \) is bounded in probability.

Then \(X\) has a modification \(Y\) which has left and right limits everywhere and such that there is a countable set \(S \subseteq T\) for which \(Y\) is right-continuous on \(T \setminus S\).

Proof

Let \(X : T \to \Omega \to \mathbb {R}\) be an adapted stochastic process which is right-continuous in probability and such that one of the two conditions of Theorem 11.2 holds. Then \(X\) has a cadlag modification.

Proof

Let \(X : T \to \Omega \to \mathbb {R}\) be a martingale which is right-continuous in probability. Then \(X\) has a cadlag modification.

Proof

Let \(X : T \to \Omega \to \mathbb {R}\) be a martingale. Then \(X\) has a modification \(Y\) such that for all \(t \in T\), \(Y\) has left and right limits at \(t\) and such that there is a countable set \(S \subseteq T\) for which \(Y\) is right-continuous on \(T \setminus S\).

Proof

Let \(X : T \to \Omega \to \mathbb {R}\) be a martingale with respect to a right-continuous filtration. Then \(X\) has a cadlag modification.

Proof

11.3 Cadlag modifications of (local) martingales

TODO: this is partially or entirely redundant, consider removing this section (and moving the dyadics definition elsewhere).

Definition 11.7 Dyadics
#

For \(T{\gt}0\), let \(\mathcal{D}_n^T = \left\lbrace \frac{k}{2^n}T \mid k=0,\cdots 2^n\right\rbrace \) be the set of dyadics at scale \(n\) and let \(\mathcal{D}^T=\bigcup _{n\in \mathbb {N}}\mathcal{D}_n^T\) be the set of all dyadics of \([0,T]\).

Let \(X=(X_t)_{t\in \mathcal{D}}\) be a martingale indexed by the dyadics. Then almost surely, for every \(t\geq 0\) the limit

\[ \lim _{\stackrel{s\rightarrow t^-}{s\in \mathcal{D}}}X_s(\omega ) \]

exists and is finite.

Proof

See 8.2.1 of Pascucci.

Let \(X=(X_t)_{t\in \mathcal{D}}\) be a martingale indexed by the dyadics. Then almost surely, for every \(t\geq 0\) the limit

\[ \lim _{\stackrel{s\rightarrow t^+}{s\in \mathcal{D}}}X_s(\omega ) \]

exists and is finite.

Proof

See 8.2.1 of Pascucci.

Let the filtered probability space satisfy the usual conditions. Then every martingale \(X\) admits a modification that is still a martingale with cadlag trajectories.

Proof

See 8.2.3 of Pascucci.

Let the filtered probability space satisfy the usual conditions. Then every nonnegative submartingale \(X\) admits a modification that is still a nonnegative submartingale with cadlag trajectories.

Proof

See 8.2.3 of Pascucci.

Lemma 11.12

Let the filtered probability space satisfy the usual conditions. Then every local martingale \(X\) admits a modification that is still a local martingale with cadlag trajectories.

Proof