Formalization of a Brownian motion and of stochastic integrals in Lean

11 Modifications with cadlag paths

11.1 Cadlag modifications of martingales

11.1.1 Stochastic intervals

Definition 11.1 Stochastic intervals
#

Let \(T\) be a time domain and let \(\sigma , \tau \) be functions \(\Omega \to T \cup \{ \infty \} \). We define

\begin{align*} [\! [\sigma , \tau ]\! ] & = \{ (t, \omega ) \in T \times \Omega \mid \sigma (\omega ) \le t \le \tau (\omega )\} \: , \\[\! [\sigma , \tau [\! [ & \ArrayCell = \{ (t, \omega ) \in T \times \Omega \mid \sigma (\omega ) \le t {\lt} \tau (\omega )\} \: , \\ ]\! ]\sigma , \tau ]\! ]\end{align*}

= {(t, ω) T ×Ω∣σ(ω) < t ≤τ(ω)}  ,
]]σ, τ[[ = {(t, ω) T ×Ω∣σ(ω) < t < τ(ω)}  ,
= {(t, ω) T ×Ω∣σ(ω) = t} = [[σ, σ]]  .

\end{align*}

We call those stochastic intervals. Note that these are subsets of \(T \times \Omega \), not of \( (T \cup \{ \infty \} ) \times \Omega \). \([\! [\sigma ]\! ]\) is called the graph of \(\sigma \).

Definition
#

If \(\sigma \) and \(\tau \) are stopping times, then the stochastic interval \(]\! ]\sigma , \tau ]\! ]\) is a predictable set.

Proof

If \(\sigma \) and \(\tau \) are bounded stopping times on \(\mathbb {N}\), then the stochastic interval \(]\! ]\sigma , \tau ]\! ]\) is an elementary predictable set.

Proof

Let \(n\) be a common upper bound for \(\sigma \) and \(\tau \). To see that the stochastic interval is an elementary predictable set, note that it can be written as a finite disjoint union of sets

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

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

11.1.2 Upcrossings

Definition 11.4
#

Let \(X : T \to \Omega \to \mathbb {R}\) be a stochastic process, \(t \in T\), and \(a, b \in \mathbb {R}\). The auxiliary lower crossing time \(\sigma '_{a, s, t}\) is the hitting time of the set \((-\infty , a]\) by the process \(X\) between times \(s\) and \(t\).

Definition 11.5 Upper crossing time
#

Let \(X : T \to \Omega \to \mathbb {R}\) be a stochastic process, \(t \in T\), and \(a, b \in \mathbb {R}\). The \(n\)-th upper crossing time \(\tau ^n_{a, b, t}\) of the interval \([a, b]\) by \(X\) before time \(t\) is the hitting time of the set \([b, \infty )\) by \(X\) after hitting the set \((-\infty , a]\) for the \(n-1\)-th time.

That is, \(\tau ^0_{a, b, t} = 0\), and for all \(n\), \(\tau ^{n+1}_{a, b, t}\) is the hitting time of \([b, \infty )\) by \(X\) between \(\sigma '_{a, \tau ^{n}_{a, b, t}, t}\) and \(t\).

Definition 11.6 Lower crossing time
#

Let \(X : T \to \Omega \to \mathbb {R}\) be a stochastic process, \(t \in T\), and \(a, b \in \mathbb {R}\). The \(n\)-th lower crossing time \(\sigma ^n_{a, b, t}\) of the interval \([a, b]\) by \(X\) before time \(t\) is the hitting time of the set \((-\infty , a]\) by \(X\) after hitting the set \([b, \infty )\) for the \(n\)-th time.

That is, it is the hitting time of \((-\infty , a]\) by \(X\) between \(\tau ^n_{a, b, t}\) and \(t\).

Definition 11.7 Upcrossings before time \(t\)
#

Let \(X : T \to \Omega \to \mathbb {R}\) be a stochastic process, \(t \in T\), and \(a, b \in \mathbb {R}\). The number of upcrossings \(U_t[a, b]\) of the interval \([a, b]\) by \(X\) before time \(t\) is the largest \(n\) such that \(\tau ^n_{a, b, t} {\lt} t\), or \(\infty \) if there is no such largest \(n\).

Definition 11.8 Upcrossings
#

Let \(X : T \to \Omega \to \mathbb {R}\) be a stochastic process and \(a, b \in \mathbb {R}\). The number of upcrossings \(U[a, b]\) of the interval \([a, b]\) by \(X\) is the supremum over \(t \in T\) of the number of upcrossings \(U_t[a, b]\) of \([a, b]\) by \(X\) before time \(t\).

Lemma 11.9
#

Let \(u : \beta \to \alpha \), for \(\alpha \) a densely ordered, conditionally complete linear order equipped with the order topology. Let \(S\) be a dense subset of \(\alpha \) and \(f\) a filter of \(\beta \). If for all \(a {\lt} b\) in \(S\), the number of upcrossings of the interval \([a, b]\) by \(u\) along \(f\) is finite, then \(u\) tends to a limit along \(f\).

Proof

For an adapted process \(X : \mathbb {N} \to \Omega \to \mathbb {R}\) indexed by the natural numbers, the upper crossing time \(\tau ^n_{a, b, t}\) is a stopping time.

Proof

For an adapted process \(X : \mathbb {N} \to \Omega \to \mathbb {R}\) indexed by the natural numbers, the lower crossing time \(\sigma ^n_{a, b, t}\) is a stopping time.

Proof

Let \(X : \mathbb {N} \to \Omega \to \mathbb {R}\) be an adapted process on the natural numbers. The upcrossing predictable set of \(X\) before time \(N\) is the predictable set defined by

\begin{align*} A_N = \bigcup _{k=0}^{N-1} ]\! ]\sigma ^k_{a, b, N}, \tau ^{k+1}_{a, b, N}]\! ] \: . \end{align*}

The upcrossing predictable set \(A_N\) of \(X : \mathbb {N} \to \Omega \to \mathbb {R}\) before time \(N\) is a predictable set.

Proof

By Lemmas 11.11 and 11.10, \(\sigma ^k_{a, b, N}\) and \(\tau ^{k+1}_{a, b, N}\) are stopping times. Hence by Lemma 11.2, the stochastic interval \(]\! ]\sigma ^k_{a, b, N}, \tau ^{k+1}_{a, b, N}]\! ]\) is a predictable set for each \(k\). Since a finite union of predictable sets is predictable, \(A_N\) is predictable.

The upcrossing predictable set \(A_N\) of \(X : \mathbb {N} \to \Omega \to \mathbb {R}\) before time \(N\) is an elementary predictable set.

Proof

By Lemmas 11.11 and 11.10, \(\sigma ^k_{a, b, N}\) and \(\tau ^{k+1}_{a, b, N}\) are stopping times, and are bounded by \(N\). By Lemma 11.3, the stochastic intervals \(]\! ]\sigma ^k_{a, b, N}, \tau ^{k+1}_{a, b, N}]\! ]\) are elementary predictable sets for each \(k\). Since a finite union of elementary predictable sets is elementary predictable, \(A_N\) is elementary predictable.

Let \(X : \mathbb {N} \to \Omega \to \mathbb {R}\) be an adapted process on the natural numbers. Then for all \(a {\lt} b\) in \(\mathbb {R}\) and \(t \in \mathbb {N}\), for \(A_t\) the upcrossing predictable set of \(X\) before time \(t\), 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_t} \bullet X)_t + \max \{ a - X_t, 0\} \: . \end{align*}
Proof
\begin{align*} (\mathbb {1}_{A_t} \bullet X)_t & = \sum _{k=0}^t (X_{\tau ^{k+1}_{a, b, t} \wedge t} - X_{\sigma ^k_{a, b, t} \wedge t}) \\ & = \sum _{k=0}^{U_t[a, b]-1} (X_{\tau ^{k+1}_{a, b, t} \wedge t} - X_{\sigma ^k_{a, b, t} \wedge t}) + (X_t - X_{\sigma ^{U_t[a, b]}_{a, b, t} \wedge t}) \\ & \ge (b - a) U_t[a, b] + \min \{ X_t - a, 0\} \\ & = (b - a) U_t[a, b] - \max \{ a - X_t, 0\} \: . \end{align*}

Let \(X : T \to \Omega \to \mathbb {R}\) be an adapted 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

Go from \(T\) to a subset of \(\mathbb {N}\) and use Lemma 11.15?

11.1.3 Cadlag modifications

Let \(X : T \to \Omega \to \mathbb {R}\) be an adapted stochastic process such that \(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. 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 \(D\) be a countable dense subset of \(T\) (e.g. the rationals in \(T\)) and let \(t \in T\) and let \(S\) be a finite subset of \(D \cap [0, t]\). By Lemma 11.16, for all \(a {\lt} b\) in \(\mathbb {R}\), the number of upcrossings \(U_S[a, b]\) of the interval \([a, b]\) along \(S\) satisfies

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

for some elementary predictable set \(A\). Taking expectations and using the boundedness hypothesis, we obtain

\begin{align*} (b - a) \mathbb {E}[U_S[a, b]] \le L + \mathbb {E}[\max \{ a - X_t, 0\} ] \le L + |a| + \mathbb {E}[|X_t|] \end{align*}

where \(L\) is a bound for \(\{ \mathbb {E}[(\mathbb {1}_A \bullet X)_t] \mid A \text{ elementary predictable}\} \).

Now, let \(S_1 \subseteq S_2 \subseteq \cdots \) be an increasing sequence of finite subsets of \(D \cap [0, t]\) with \(\bigcup _n S_n = D \cap [0, t]\). The number of upcrossings \(U_{S_n}[a, b]\) is increasing in \(n\). By monotone convergence,

\begin{align*} (b - a) \mathbb {E}[U_{D \cap [0, t]}[a, b]] = \lim _{n \to \infty } (b - a) \mathbb {E}[U_{S_n}[a, b]] \le L + |a| + \mathbb {E}[|X_t|] {\lt} \infty . \end{align*}

In particular, \(U_{D \cap [0, t]}[a, b] {\lt} \infty \) a.s. for each pair \(a {\lt} b\). Since \(\mathbb {Q}^2\) is countable, we conclude that almost surely, for all rational \(a {\lt} b\), the number of upcrossings of \([a, b]\) by \(X\) along \(D \cap [0, t]\) is finite.

By Lemma 11.9, finite upcrossings of all rational intervals implies that the left and right limits of \(s \mapsto X_s(\omega )\) along \(D\) exist at every \(t \in T\), for almost every \(\omega \). Define

\[ \tilde{Y}_t(\omega ) = \lim _{\substack {s \downarrow t \\ s \in D}} X_s(\omega ) \]

whenever this limit exists, and \(\tilde{Y}_t(\omega ) = 0\) otherwise. Then \(\tilde{Y}\) has left and right limits everywhere (along \(T\)) almost surely, and is right-continuous at every point of \(D\).

We claim that the set

\begin{align*} S = \{ t \in T \mid \tilde{Y}_t \ne X_t \text{ with positive probability}\} \end{align*}

is countable. For each \(n \in \mathbb {N}\), consider the set

\begin{align*} S_n = \{ t \in T \cap [0, n] \mid \mathbb {P}(|\tilde{Y}_t - X_t| {\gt} 1/n) {\gt} 1/n\} \: . \end{align*}

We have \(S = \bigcup _n S_n\), so it suffices to show each \(S_n\) is finite. If \(S_n\) were infinite, it would contain a monotone sequence \(t_k\) converging to some limit \(t^* \in [0, n]\). Adding \(\{ t_k\} \) to \(D\) and repeating the upcrossing argument, we would obtain that \(X_{t_k}\) converges along \(D \cup \{ t_k\} \) almost surely. But \(\tilde{Y}_{t_k}\) also converges (since \(\tilde{Y}\) has left/right limits), giving \(\tilde{Y}_{t_k} - X_{t_k} \to 0\) in probability, contradicting the definition of \(S_n\). Therefore each \(S_n\) is finite and \(S\) is countable.

Define

\begin{align*} Y_t = \begin{cases} X_t & \text{if } t \in S \: , \\ \tilde{Y}_t & \text{if } t \notin S \: . \end{cases}\end{align*}

Then \(Y_t = X_t\) almost surely for all \(t\): for \(t \in S\) this is by definition, and for \(t \notin S\) this follows from \(\tilde{Y}_t = X_t\) a.s. Thus \(Y\) is a modification of \(X\).

Since \(\tilde{Y}\) has left and right limits everywhere almost surely, and \(Y\) differs from \(\tilde{Y}\) only on the countable set \(S\), \(Y\) also has left and right limits everywhere almost surely. Furthermore, \(Y\) agrees with \(\tilde{Y}\) on \(T \setminus S\), so \(Y\) is right-continuous on \(T \setminus S\).

In the following, we say that a stochastic process \(X\) is right-continuous in probability if for all \(t \in T\), \(\lim _{s \downarrow t} X_s = X_t\) in which the limit is taken in probability.

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

Proof

Let \(Y\) be the modification of \(X\) given by Theorem 11.17. \(Y\) has left and right limits everywhere and there is a countable set \(S\) such that \(Y\) is right-continuous on \(T \setminus S\). It remains to show that \(Y\) is right-continuous at the points of \(S\). Let \(Y_{t+}\) denote the right limit of \(Y\) at \(t\). Since \(X\) is right-continuous in probability, for all \(t \in S\), \(Y_t = Y_{t+}\) almost surely. Therefore, since \(S\) is countable, we have that almost surely \(Y_t = Y_{t+}\) for all \(t \in S\) (and hence for all \(t \in T\)). \(Y\) is therefore almost surely cadlag. We can modify \(Y\) on the null set to obtain a cadlag modification of \(X\).

Let \(X : T \to \Omega \to \mathbb {R}\) be a submartingale. Then for every \(t \in T\), the set \(\{ \mathbb {E}[(\mathbb {1}_A \bullet X)_t] \mid A \text{ elementary predictable}\} \) is bounded.

Proof

Since \(X\) is a submartingale, for any elementary predictable set \(A\), we have (Corollary 10.26)

\begin{align*} 0 \le \mathbb {E}[(\mathbb {1}_A \bullet X)_t] \le \mathbb {E}[X_t - X_0] \: . \end{align*}

As \(X_t\) and \(X_0\) are integrable, the set \(\{ \mathbb {E}[(\mathbb {1}_A \bullet X)_t] \mid A \text{ elementary predictable}\} \) is bounded.

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

Proof

We apply Corollary 11.18, in which the boundedness condition of Theorem 11.17 holds by Lemma 11.19.

Let \(X : T \to \Omega \to \mathbb {R}\) be a submartingale. 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

Apply Theorem 11.17, in which the boundedness condition holds by Lemma 11.19.

Lemma 11.22

Let \(X : T \to \Omega \to \mathbb {R}\) be a submartingale and let \(t_n\) be a decreasing sequence in \(T\) which is bounded below. Then the family \(\{ X_{t_n}\} _{n \in \mathbb {N}}\) is uniformly integrable.

Proof
Lemma 11.23

Let \(X : T \to \Omega \to \mathbb {R}\) be a submartingale and \(t \in T\). Let \(t_n\) be a decreasing sequence in \(T\) converging to \(t\), and such that \(X_{t_n}\) tends to a limit \(X_{t+}\) almost surely. Then \(X_t \le P[X_{t+} \mid \mathcal{F}_t]\) almost surely.

Proof

By the submartingale property, for all \(n\) we have that \(X_t \le P[X_{t_n} \mid \mathcal{F}_t]\) almost surely. By Lemma 11.22, the family \(\{ X_{t_n}\} _{n \in \mathbb {N}}\) is uniformly integrable.

TODO: conclude that \(P[X_{t+} \mid \mathcal{F}_t]\) is the limit of \(P[X_{t_n} \mid \mathcal{F}_t]\).

Let \(X : T \to \Omega \to \mathbb {R}\) be a submartingale with respect to a right-continuous filtration. Then \(X\) has a cadlag modification if and only if \(t \mapsto \mathbb {E}[X_t]\) is right-continuous.

Proof

Let \(Y\) be the modification of \(X\) given by Lemma 11.21. \(Y\) has left and right limits everywhere and there is a countable set \(S\) such that \(Y\) is right-continuous on \(T \setminus S\). It remains to show that for each \(t \in S\), \(Y\) is right-continuous at \(t\) almost surely. We will then be able to modify \(Y\) on a null set to obtain a cadlag modification of \(X\). Let \(t \in S\) and let \(Y_{t+}\) denote the right limit of \(Y\) at \(t\).

We show that \(Y_t = P[Y_{t+} \mid \mathcal{F}_t]\) almost surely, and that \(P[Y_{t+} \mid \mathcal{F}_t] = Y_{t+}\) almost surely, which will conclude the proof. For the second equality it suffices to show that \(Y_{t+}\) is \(\mathcal{F}_t\)-measurable, which follows from the right-continuity of the filtration.

For the first equality, it suffices to show that \(P[Y_{t+} \mid \mathcal{F}_t] - Y_t\) is an almost surely nonnegative random variable with zero expectation. Nonnegative follows from Lemma 11.23. The expectation is \(P[Y_{t+}] - P[Y_t]\). Let \(t_n\) be a decreasing sequence in \(T\) converging to \(t\). By right-continuity of \(t \mapsto \mathbb {E}[Y_t]\), we have that

\begin{align*} P[Y_t] = \lim _{n \to \infty } P[Y_{t_n}] \: . \end{align*}

By uniform integrability (Lemma 11.22), we have that

\begin{align*} P[Y_{t+}] = \lim _{n \to \infty } P[Y_{t_n}] \: . \end{align*}

Therefore \(P[Y_{t+}] = P[Y_t]\), which concludes the 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

\(X\) is in particular a submartingale, and for all \(t \in T\), we have that \(\mathbb {E}[X_t] = \mathbb {E}[X_0]\) by the martingale property. Therefore \(t \mapsto \mathbb {E}[X_t]\) is right-continuous, and we can apply Theorem 11.24.

11.2 Cadlag modifications of (local) martingales

TODO: this is partially or entirely redundant, consider removing this section.

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.27

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