Formalization of a Brownian motion and of stochastic integrals in Lean

13 Classes of martingales and related processes

The main reference for this part is [ HWY19 ] .

Notations for classes of processes:

  • \(\mathcal{V}\): finite variation processes (Definition 13.9)

  • \(\mathcal{V}^+\): non-decreasing finite variation processes

  • \(\mathcal{A}\): adapted processes with integrable variation (Definition 13.14)

  • \(\mathcal{A}^+\): non-decreasing adapted integrable processes

  • \(\mathcal{M}\): càdlàg martingales (TODO: [ HWY19 ] add uniform integrability)

  • \(\mathcal{M}^c\): continuous martingales

  • \(\mathcal{M}^2\): square-integrable martingales (Definition 13.15)

  • \(\mathcal{C}_{\mathrm{loc}}\) for a class \(\mathcal{C}\): processes that are locally in \(\mathcal{C}\)

Note: [ HWY19 ] use \(\mathcal{W}\) for \(\mathcal{M} \cap \mathcal{A}\).

13.1 Jumps of a process

Definition 13.1 Jumps of a process
#

The jumps of a process \(X : T \to \Omega \to E\) is the process \(\Delta X : T \to \Omega \to E\) defined by \((t, \omega ) \mapsto X_t(\omega ) - X_{t^-}(\omega )\) .

Definition 13.2 Jump part

The jump part (or purely discontinuous part) of a process \(X : T \to \Omega \to E\) is the process \(X^d : T \to \Omega \to E\) defined by \((t, \omega ) \mapsto \sum _{0 {\lt} s \le t} \Delta X_s(\omega )\) .

Definition 13.3 Continuous part

The continuous part of a process \(X : T \to \Omega \to E\) is the process \(X^c : T \to \Omega \to E\) defined by \((t, \omega ) \mapsto X_t(\omega ) - X^d_t(\omega )\) .

Definition 13.4 Large jumps

The large jump part of a process \(X : T \to \Omega \to E\) at level \(\varepsilon \) is the process \(X^{d, \varepsilon } : T \to \Omega \to E\) defined by \((t, \omega ) \mapsto \sum _{0 {\lt} s \le t} \Delta X_s(\omega ) \mathbb {1}_{\{ \Vert \Delta X_s(\omega ) \Vert {\gt} \varepsilon \} }\) .

13.2 Integrable variation

Definition 13.5 Extended variation
#

The (extended-real-valued) variation of a function \(f : T \to E\) on a set \(s\) inside a linear order is the supremum of \(\sum _i \mathrm{edist}(f(u_{i+1}, f(u_i)))\) over all finite increasing sequences \(u : N \to T\) in \(s\). We denote it by \(V_f(s)\) .

Definition 13.6 Bounded variation
#

A function \(f : T \to E\) is of bounded variation on a set \(s\) if its variation \(V_f(s)\) is finite.

Definition 13.7 Locally bounded variation
#

A function \(f : T \to E\) is of locally bounded variation on a set \(s\) if for every \(a, b\) in \(s\), the variation \(V_f(s \cap [a, b])\) is finite.

Lemma 13.8

The set of points of discontinuity of a function of locally bounded variation is at most countable.

Proof

Mathlib has the result for monotone functions and has the fact that a function of locally bounded variation is the difference of two monotone functions.

Definition 13.9 Finite variation process, \(\mathcal{V}\)

A process \(X : T \to \Omega \to E\) is of finite variation if it is right-continuous and for every \(\omega \in \Omega \), the path \(t \mapsto X_t(\omega )\) is of locally bounded variation on \(T\) .

We denote by \(\mathcal{V}\) the class of finite variation processes.

A finite variation process is càdlàg.

Proof

Right-continuity is by definition. Left limits exist because a function of locally bounded variation has left limits (that should be in Mathlib’s file about locally bounded variation).

Definition 13.11

The variation of a process \(X : T \to \Omega \to E\) is the process \(V_X : T \to \Omega \to \mathbb {R}\) defined by \((t, \omega ) \mapsto V_{X(\omega )}([0,t])\) .

Lemma 13.12

The variation process \(V_X\) of a process \(X\) is non-decreasing.

Proof
Lemma 13.13

The variation process \(V_X\) of a right-continuous process \(X\) is right-continuous.

Proof
Definition 13.14 Integrable variation, \(\mathcal{A}\)

We say that a stochastic process \(X\) has integrable variation if its variation process \(V_X\) (Definition 13.11) is integrable (Definition 9.31).

We denote by \(\mathcal{A}\) the class of adapted processes with integrable variation.

We denote by \(\mathcal{A}^+\) the class of non-decreasing adapted integrable processes.

We denote by \(\mathcal{V}^+\) the class of non-decreasing adapted processes.

13.3 Square integrable martingales

In this section, \(E\) denotes a complete normed space.

Definition 13.15 Square integrable martingales
#

Let \(T\) be a linear order with bottom element 0, on which we have a filtration \(\mathcal{F}\) satisfying the usual conditions. We say that a martingale \(M : T \to \Omega \to E\) is square integrable if it is càdlàg and \(\sup _{t \in T} \Vert M_t \Vert _{L^2} {\lt} \infty \) (Lean remark: use eLpNorm (M t) 2).

13.3.1 The Hilbert space of square integrable martingales

If \(M\) and \(N\) are square integrable martingales and \(a \in \mathbb {R}\), then \(M + N\) and \(a M\) are square integrable martingales.

Proof

If \(M\) is a square integrable martingale, then \(\Vert M \Vert ^2\) is a submartingale.

Proof

Apply Lemma 7.15 with the convex function \(f: x \mapsto \Vert x \Vert ^2\) .

Lemma 13.18

For \(M\) a square integrable martingale, the function \(t \mapsto \Vert M_t \Vert _{L^2}\) is non-decreasing.

Proof

By Lemma 13.17, \(\Vert M_t \Vert ^2\) is a submartingale. Thus, for \(s \le t\) ,

\begin{align*} \Vert M_s \Vert _{L^2}^2 & = \mathbb {E}[\Vert M_s \Vert ^2] \\ & \le \mathbb {E}[\Vert M_t \Vert ^2] \\ & = \Vert M_t \Vert _{L^2}^2 \: . \end{align*}

For \(M\) a square integrable martingale, we have \(M_t \to M_\infty \) almost surely and in \(L^2\) as \(t \to \infty \) .

Proof

TODO: use a martingale convergence theorem. Check whether Theorem 7.83 is what we need.

For \(M\) a square integrable martingale,

\begin{align*} \sup _{t \in T} \Vert M_t \Vert _{L^2} & = \Vert M_\infty \Vert _{L^2} \: . \end{align*}
Proof
Definition 13.21

We denote by \(\mathcal{M}^2(E)\) or simply \(\mathcal{M}^2\) the space of equivalence classes with respect to indistinguishability of square integrable martingales \(T \to \Omega \to E\) .

Lemma 13.22

The space \(\mathcal{M}^2(E)\) is a real vector space.

Proof
Definition 13.23

We define a norm on \(\mathcal{M}^2\) by

\begin{align*} \Vert M \Vert = \Vert M_\infty \Vert _{L^2} \: . \end{align*}
Lemma 13.24

For \(M \in \mathcal{M}^2(E)\), \(\Vert M \Vert = 0\) if and only if \(M = 0\).

Proof

By Lemma 13.20, \(\Vert M \Vert = 0\) if and only if for all \(t \in T\), \(\Vert M_t \Vert _{L^2} = 0\) .

Definition 13.25

We define an inner product on \(\mathcal{M}^2\) by

\begin{align*} \langle M, N \rangle _{\mathcal{M}^2} = \mathbb {E}[M_\infty N_\infty ] \: . \end{align*}

The space \(\mathcal{M}^2\) is a Hilbert space.

Proof

We already know that \(\mathcal{M}^2\) is an inner product space. We need to show that it is complete.

It suffices to show that every Cauchy sequence with a distance bound converges to a limit in \(\mathcal{M}^2\). Namely, we can consider sequences \((M^n)_{n \in \mathbb {N}}\) in \(\mathcal{M}^2\) such that for \(n, m \ge N\), \(\Vert M^n - M^m \Vert {\lt} 2^{-N}\) (See Metric.complete_of_convergent_controlled_sequences, or the EMetric version).

Let then \((M^n)_{n \in \mathbb {N}}\) be such a Cauchy sequence.

TODO

13.3.2 Elementary stochastic integrals

For \(V \in \mathcal{E}_{T, F}\) bounded by a constant \(D\), \(M \in \mathcal{M}^2(E)\) and a continuous bilinear map \(B: E \times F \to G\),

\begin{align*} \Vert (V \bullet _B M)_t \Vert _{L^2} \le 2 D \: \Vert B \Vert \: \sup _t \Vert M_t \Vert _{L^2} \end{align*}

TODO: this can be improved to \(D \: \Vert B \Vert \: \Vert M_t \Vert _{L^2}\)?

Proof

Let \(C\) be a bound on \(\Vert M_t \Vert _{L^2}\) for all \(t \in T\) . Let \((s_k {\lt} t_k)_{k \in \{ 1, ..., n\} }\) and \(\eta _k\) be the intervals and random variables defining \(V\) . Let \(D\) be a bound on \(\Vert \eta _k\Vert \). Then, for all \(t\) ,

\begin{align*} \Vert (V \bullet _B M)_t \Vert _{L^2} & \le \sum _{k=1}^n \Vert B(M^t_{t_k} - M^t_{s_k}, \eta _k) \Vert _{L^2} \: . \end{align*}

Since only at most one term of that sum is non-zero for each fixed \(t\) , we can bound the sum by the maximum of its terms. It suffices then to bound each term of that sum.

TODO: here we supposed that the intervals of the simple process are disjoint. Check with our Lean def.

For each \(k\) ,

\begin{align*} \Vert B(M^t_{t_k} - M^t_{s_k}, \eta _k) \Vert _{L^2} & \le \left\Vert \Vert B \Vert \: \Vert M^t_{t_k} - M^t_{s_k} \Vert \: \Vert \eta _k \Vert \right\Vert _{L^2} \\ & \le \Vert B \Vert \: \Vert M^t_{t_k} - M^t_{s_k} \Vert _{L^2} \: D \\ & \le 2 \Vert B \Vert \: C \: D \: . \end{align*}

For \(V \in \mathcal{E}_{T, F}\), \(M \in \mathcal{M}^2(E)\) and a continuous bilinear map \(B: E \times F \to G\), the elementary stochastic integral \(V \bullet _B M\) is in \(\mathcal{M}^2(G)\).

Proof

By Lemma 10.34, \(V \bullet _B M\) is càdlàg, and we know that it is a martingale by Lemma 10.44 . It remains to show that \(\sup _{t \in T} \Vert (V \bullet _B M)_t \Vert _{L^2} {\lt} \infty \) . By Lemma 13.27, this supremum is bounded by \(2 D \Vert B \Vert \sup _{t \in T} \Vert M_t \Vert _{L^2}\), which is finite since \(M \in \mathcal{M}^2(E)\) and \(V\) is bounded.

For \(V \in \mathcal{E}_{T, \mathbb {R}}\) and \(M, N \in \mathcal{M}^2\), we have

\begin{align*} \langle V \bullet _{\mathbb {R}} M, N \rangle _{\mathcal{M}^2} & = V \bullet _{\mathbb {R}} \langle M, N \rangle _{\mathcal{M}^2} \: . \end{align*}
Proof

13.4 Locally square integrable martingales

13.4.1 Definition and basic properties

Definition 13.30 Locally square-integrable martingales

A process is locally square-integrable if it locally satisfies the square-integrable martingale property. We denote that class of processes by \(\mathcal{M}^2_{\mathrm{loc}}\) .

Every square-integrable martingale is locally square-integrable: \(\mathcal{M}^2 \subseteq \mathcal{M}^2_{\mathrm{loc}}\) .

Proof

This follows from Lemma 9.9.

If \(M \in \mathcal{M}^2_{\mathrm{loc}}\), then \(\Vert M \Vert ^2\) is a càdlàg local submartingale.

Proof

A continuous local martingale is locally square-integrable: \(\mathcal{M}^c_{\mathrm{loc}} \subseteq \mathcal{M}^2_{\mathrm{loc}}\) .

Proof

13.4.2 Predictable quadratic variation

Definition 13.34 Predictable quadratic variation

For \(M \in \mathcal{M}^2_{\mathrm{loc}}\) with càdlàg paths, the predictable quadratic variation of \(M\) is defined as the predictable part of the Doob-Meyer decomposition of the local submartingale \(\Vert M \Vert ^2\) . We denote it by \(\langle M \rangle \) .

The predictable quadratic variation \(\langle M \rangle \) of \(M \in \mathcal{M}^2_{\mathrm{loc}}\) is a predictable process.

Proof

The predictable quadratic variation \(\langle M \rangle \) of \(M \in \mathcal{M}^2_{\mathrm{loc}}\) is càdlàg.

Proof

The predictable quadratic variation \(\langle M \rangle \) of \(M \in \mathcal{M}^2_{\mathrm{loc}}\) is locally integrable.

Proof

\(\langle M \rangle _0 = 0\) .

Proof

The predictable quadratic variation \(\langle M \rangle \) of \(M \in \mathcal{M}^2_{\mathrm{loc}}\) is non-decreasing.

Proof

For \(M \in \mathcal{M}^2_{\mathrm{loc}}\), the process \(\Vert M_t \Vert ^2 - \langle M \rangle _t\) is a local martingale.

Proof
Definition 13.41 Predictable covariation

For \(M, N \in \mathcal{M}^2_{\mathrm{loc}}\), the predictable covariation \(\langle M, N \rangle \) is a stochastic process defined by polarization of the predictable quadratic variation:

\begin{align*} \langle M, N \rangle _t = \frac{1}{4}\left(\langle M+N \rangle _t - \langle M-N \rangle _t \right) \: . \end{align*}
Lemma 13.42

The predictable covariation \(\langle M, N \rangle \) of \(M, N \in \mathcal{M}^2_{\mathrm{loc}}\) is a predictable process.

Proof
Lemma 13.43

The predictable covariation \(\langle M, N \rangle \) of \(M, N \in \mathcal{M}^2_{\mathrm{loc}}\) is càdlàg.

Proof
Lemma 13.44

\(\langle M, N \rangle _0 = 0\) .

Proof
Lemma 13.45

For \(M, N \in \mathcal{M}^2_{\mathrm{loc}}\), the process \(\langle M_t, N_t \rangle _E - \langle M, N \rangle _t\) is a local martingale.

Proof
\begin{align*} & \langle M_t, N_t \rangle _E - \langle M, N \rangle _t \\ & = \frac{1}{4}\left( \left(\Vert M_t + N_t \Vert ^2 - \langle M+N \rangle _t\right) - \left(\Vert M_t - N_t \Vert ^2 - \langle M-N \rangle _t\right) \right) \: . \end{align*}

The two differences are local martingales by Lemma 13.40, so their linear combination is also a local martingale.

Let \(M\) and \(N\) be square integrable martingales. Then

\begin{align*} \mathbb {E}\left[\langle M,N \rangle _\infty \right] = \langle M - M_0, N - N_0 \rangle _{\mathcal{M}^2} \: . \end{align*}
Proof
Lemma 13.47

Let \(B\) be a standard Brownian motion. Then the quadratic variation of \(B\) is given by \(\langle B \rangle _t = t\) .

Proof

13.5 Local martingales

The large jump process of a local martingale is a process with locally integrable variation (it’s in \((\mathcal{A} \cap \mathcal{M})_{\mathrm{loc}}\)).

Proof
Theorem 13.49

Let \(M\) be a local martingale. Then for any \(\varepsilon {\gt} 0\), \(M\) can be decomposed as \(M = M_0 + U + V\), where \(U\) is a locally bounded martingale (local version of both bounded and martingale) with \(\vert \Delta U \vert \le \varepsilon \) and \(U_0 = 0\) and \(V\) is a local martingale with locally integrable variation (\(V \in (\mathcal{M} \cap \mathcal{A})_{\mathrm{loc}}\)) and \(V_0 = 0\).

Proof

See [ HWY19 ] , 7.17

Remark: \(U\) is locally bounded, hence locally square integrable, so we can use the integration machinery for those to define an integral. \(V\) has locally integrable variation so we can integrate it with Stieltjes integrals.

13.6 Semimartingales

Definition 13.50 Semimartingale

A process \(X\) is a semimartingale if it can be decomposed as \(X = M + A\), where \(M\) is a local martingale (\(M \in \mathcal{M}_{\mathrm{loc}}\)) and \(A\) is an adapted process with finite variation.

TODO: it’s adapted and cadlag.

A semimartingale \(X\) can be decomposed as \(X = M + A\), where \(M\) is a locally bounded martingale with bounded jumps and \(A\) is an adapted process with finite variation.

Proof

Decompose \(X = M + A\) as in Definition 13.50. Then decompose \(M\) as in Theorem 13.49 with \(\varepsilon = 1\). Then \(M = M_0 + U + V\) with \(U\) a locally bounded martingale with \(\vert \Delta U \vert \le 1\) and \(V\) a local martingale with locally integrable variation. Then \(X = (M_0 + U) + (A + V)\), with \(U\) a locally bounded martingale with bounded jumps and \(A + V\) an adapted process of finite variation (since \(V\) has locally integrable variation, hence finite variation).

Definition 13.52 Continuous martingale part

TODO. Denoted by \(X^c\).

Definition 13.53 Quadratic covariation of semimartingales

Let \(X\) and \(Y\) be semimartingales. Their quadratic covariation \([X, Y]\) is defined as

\begin{align*} [X, Y]_t = X_0 Y_0 + \langle X^c, Y^c \rangle _t + \sum _{0 {\lt} s \le t} \Delta X_s \Delta Y_s \: . \end{align*}

TODO: this is an adapted process with finite variation (it’s in \(\mathcal{V}\)).

Definition 13.54 Quadratic variation of a semimartingale

The quadratic variation of a semimartingale \(X\) is defined as \([X] = [X, X]\) .

TODO: \([X]\) is an adapted increasing process.

Definition 13.55 Special semimartingale

A semimartingale \(X\) is a special semimartingale if it can be decomposed as \(X = M + A\), where \(M\) is a local martingale and \(A\) is an adapted process with locally integrable variation.

Theorem 13.56

A special semimartingale \(X\) can be decomposed as \(X = M + A\), where \(M\) is a local martingale and \(A\) is a predictable process with finite variation and \(A_0 = 0\).

Proof