Formalization of a Brownian motion and of stochastic integrals in Lean

9 Stochastic integral

The lecture notes at this link as well as chapter 18 of [ are good references for this chapter. Some of the proofs are taken from [ .

9.1 Total variation and Lebesgue-Stieltjes integral

TODO: in Mathlib, we can integrate with respect to the measure given by a right-continuous monotone function (StieltjesFunction.measure). This will be useful to integrate against the quadratic variation of a local martingale. However, we will also want to integrate with respect to a signed measure given by a càdlàg function with finite variation. We need to investigate what’s already in Mathlib. See Mathlib.Topology.EMetricSpace.BoundedVariation.

9.2 Doob’s Lp inequality

In this section, we prove Doob’s Lp inequality.

Lemma 9.1

Let \(X:T\times \Omega \rightarrow E\) a martingale with values in a normed space \(E\). Let \(\phi : E \rightarrow \mathbb {R}\) convex such that \(\phi (X_t)\in L^1(\Omega )\) for every \(t\in T\). Then \(\phi (X)\) is a sub-martingale.

Proof

By the conditional Jensen’s inequality (see #27953) \(\phi (X_t) = \phi \left( \mathbb {E}[X_T\ |\ \mathcal{F}_t] \right)\leq \mathbb {E}[\phi (X_T)\ |\ \mathcal{F}_t]\).

Lemma 9.2

Let \(X:T\times \Omega \rightarrow \mathbb {R}^d\) a sub-martingale. Let \(\phi :\mathbb {R^d}\rightarrow \mathbb {R}\) convex increasing such that \(\phi (X_t)\in L^1(\Omega )\) for every \(t\in T\). Then \(\phi (X)\) is a sub-martingale.

Proof

By Jensen and the fact that \(\phi \) is increasing \(\phi (X_t) \leq \phi \left( \mathbb {E}[X_T\ |\ \mathcal{F}_t] \right)\leq \mathbb {E}[\phi (X_T)\ |\ \mathcal{F}_t]\).

Lemma 9.3 Doob Inequality for countable

Let \(X:I\times \Omega \rightarrow \mathbb {R}\) be a non-negative sub-martingale. Let \(I\) be countable. For every \(M\in I,\lambda {\gt} 0\) and \(p{\gt}1\) we have

\[ P\left( \sup _{i\in I, i\leq M}X_i\geq \lambda \right)\leq \frac{\mathbb {E}[X_M]}{\lambda }. \]
Proof

See 8.1.1 Pascucci.

Lemma 9.4 Doob Inequality Corollary for countable

Let \(X:I\times \Omega \rightarrow \mathbb {R}\) be a sub-martingale. Let \(I\) be countable. For every \(M\in I,\lambda {\gt} 0\) and \(p{\gt}1\) we have

\[ \mathbb {E}\left[ \sup _{i\in I, i\leq M}X_i^p \right]\leq \left(\frac{p}{p-1}\right)^p\mathbb {E}[X_M^p]. \]
Proof

8.1.1 Pascucci.

Theorem 9.5 Doob Inequality

Let \(X:\mathbb {R}\times \Omega \rightarrow \mathbb {R}\) be a right-continuous non-negative sub-martingale. For every \(T, \lambda {\gt}0\) and \(p{\gt}1\) we have

\[ P\left( \sup _{t\in [0,T]}X_t\geq \lambda \right)\leq \frac{\mathbb {E}[X_T]}{\lambda }. \]
Proof

8.1.2 Pascucci.

Corollary 9.6 Doob Inequality for normed spaces

Let \(X:\mathbb {R}\times \Omega \rightarrow E\) be a right-continuous martingale with values in a normed space \(E\). For every \(T, \lambda {\gt}0\) and \(p{\gt}1\) we have

\[ P\left( \sup _{t\in [0,T]} \lVert X_t \rVert \geq \lambda \right) \leq \frac{\mathbb {E}[\lVert X_T \rVert ]}{\lambda }. \]
Proof

By Lemma 9.1, \(\lVert X \rVert \) is a sub-martingale. Then apply Theorem 9.5.

Theorem 9.7 Doob’s Lp inequality

Let \(X:\mathbb {R}\times \Omega \rightarrow \mathbb {R}\) be a right-continuous non-negative sub-martingale. For every \(T, \lambda {\gt}0\) and \(p{\gt}1\) we have

\[ \mathbb {E}\left[ \sup _{t\in [0,T]}X_t^p \right]\leq \left(\frac{p}{p-1}\right)^p\mathbb {E}[X_T^p]. \]
Proof

8.1.2 Pascucci.

Corollary 9.8 Doob’s Lp inequality for normed spaces

Let \(X : \mathbb {R}\times \Omega \rightarrow E\) be a right-continuous martingale with values in a normed space \(E\). For every \(T, \lambda {\gt}0\) and \(p{\gt}1\) we have

\[ \mathbb {E}\left[ \sup _{t\in [0,T]} \lVert X_t \rVert ^p \right]\leq \left(\frac{p}{p-1}\right)^p\mathbb {E}[\lVert X_T \rVert ^p]. \]
Proof

By Lemma 9.1, \(\lVert X \rVert \) is a sub-martingale. Then apply Theorem 9.7.

Lemma 9.9 Stopped Martingale
#

Let \(X:\mathbb {R}\times \Omega \rightarrow \mathbb {R}\) be a cadlag martingale and \(\tau _0\) a stopping time. Then \((X_{t\wedge \tau _0})_{t\geq 0}\) is a martingale.

Lemma 9.10 Doob Inequality for stopping times

Let \(X:\mathbb {R}\times \Omega \rightarrow \mathbb {R}\) be a right-continuous non-negative sub-martingale. For every \(\lambda {\gt}0\) and \(p{\gt}1\) and \(\tau \) stopping time a.s. bounded by \(T{\gt}0\), we have

\[ P\left( \sup _{t\in [0,\tau ]}X_t\geq \lambda \right)\leq \frac{\mathbb {E}[X_\tau ]}{\lambda }. \]
Proof

Almost already in mathlib MeasureTheory.Submartingale.stoppedProcess.

Corollary 9.11 Doob Inequality for stopping times in normed spaces

Let \(X:\mathbb {R}\times \Omega \rightarrow E\) be a right-continuous martingale with values in a normed space \(E\). For every \(\lambda {\gt}0\) and \(p{\gt}1\) and \(\tau \) stopping time a.s. bounded by \(T{\gt}0\), we have

\[ P\left( \sup _{t\in [0,\tau ]}\lVert X_t \rVert \geq \lambda \right)\leq \frac{\mathbb {E}[\lVert X_\tau \rVert ]}{\lambda }. \]
Proof

By Lemma 9.1, \(\lVert X \rVert \) is a sub-martingale. Then apply Theorem 9.10.

Lemma 9.12 Doob’s Lp Inequality for stopping times

Let \(X:\mathbb {R}\times \Omega \rightarrow \mathbb {R}\) be a right-continuous non-negative sub-martingale. For every \(\lambda {\gt}0\) and \(p{\gt}1\) and \(\tau \) stopping time a.s. bounded by \(T{\gt}0\), we have

\[ \mathbb {E}\left[ \sup _{t\in [0,\tau ]}X_t^p \right]\leq \left(\frac{p}{p-1}\right)^p\mathbb {E}[X_\tau ^p]. \]
Proof

8.1.3 Pascucci.

Corollary 9.13 Doob’s Lp Inequality for stopping times in normed spaces

Let \(X:\mathbb {R}\times \Omega \rightarrow E\) be a right-continuous martingale with values in a normed space \(E\). For every \(\lambda {\gt}0\) and \(p{\gt}1\) and \(\tau \) stopping time a.s. bounded by \(T{\gt}0\), we have

\[ \mathbb {E}\left[ \sup _{t\in [0,\tau ]}\lVert X_t \rVert ^p \right]\leq \left(\frac{p}{p-1}\right)^p\mathbb {E}[\lVert X_\tau \rVert ^p]. \]
Proof

By Lemma 9.1, \(\lVert X \rVert \) is a sub-martingale. Then apply Theorem 9.12.

9.3 Square integrable martingales

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

Definition 9.14 Square integrable martingales

Let \(\mathcal{M}^2\) be the set of square integrable continuous martingales with respect to a filtration \(\mathcal{F}\) indexed by \(\mathbb {R}_+\),

\begin{align*} \mathcal{M}^2 = \{ M : \mathbb {R}_+ \to \Omega \to \mathbb {R} \mid M \text{ continuous martingale with } \sup _{t}\mathbb {E}[M_t^2] {\lt} \infty \} \: . \end{align*}
Theorem 9.15

The space \(\mathcal{M}^2\) is a Hilbert space with the inner product defined by

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

9.4 Local martingales

TODO: filtrations should be assumed right-continuous and complete whenever needed.

Definition 9.16 Quadratic variation

For any continuous local martingale \(M\), there exists a continuous process \([M]\) with \([M]_0 = 0\) such that \(M^2 - [M]\) is a local martingale. That process is a.s. unique and is called the quadratic variation of \(M\).

Definition 9.17 Covariation

For any continuous local martingales \(M\) and \(N\), there exists a continuous process \([M,N]\) with \([M,N]_0 = 0\) such that \(MN - [M,N]\) is a local martingale. That process is a.s. unique and is called the covariation of \(M\) and \(N\).

It can be defined by \([M, N]_t = \frac{1}{4}\left([M+N]_t - [M-N]_t \right)\) .

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

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

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

Proof
Definition 9.20 Continuous semi-martingale

A continuous semi-martingale is a process that can be decomposed into a local martingale and a finite variation process. More formally, a process \(X : \mathbb {R}_+ \to \Omega \to E\) is a continuous semi-martingale if there exists a continuous local martingale \(M\) and a continuous adapted process \(A\) with locally finite variation and \(A_0 = 0\) such that

\begin{align*} X_t = M_t + A_t \end{align*}

for all \(t \ge 0\). The decomposition is a.s. unique.

9.5 Stochastic integral

Definition 9.21 Simple process
#

Let \(0 \le t_0 \le t_1 \le \ldots \le t_n\) in \(\mathbb {R}_+\). Let \((\eta _k)_{0 \le k \le n-1}\) be \(\mathcal{F}_{t_k}\)-measurable random variables. Then the simple process for that sequence is the process \(V : \mathbb {R}_+ \to \Omega \to E\) defined by

\begin{align*} V_t = \sum _{k=0}^{n-1} \eta _k \mathbb {1}_{(t_k, t_{k+1}]}(t) \: . \end{align*}

Let \(\mathcal{E}\) be the set of simple processes.

Definition 9.22 Elementary stochastic integral

Let \(V \in \mathcal{E}\) be a simple process and let \(X\) be a stochastic process. The elementary stochastic integral process \(V \cdot X : \mathbb {R}_+ \to \Omega \to E\) is defined by

\begin{align*} (V \cdot X)_t & = \sum _{k=0}^{n-1} \eta _k (X^t_{t_{k+1}} - X^t_{t_k}) \: . \end{align*}
Lemma 9.23

For \(V \in \mathcal{E}\) and \(M \in \mathcal{M}^2\), then \(V \cdot M \in \mathcal{M}^2\) and

\begin{align*} \Vert V \cdot M \Vert _{\mathcal{M}^2}^2 & = \mathbb {E}\left[ \int _0^{\infty } V_t^2 \: d[M]_t \right] \: . \end{align*}
Proof

9.5.1 Itô isometry

Definition 9.24

Let \(M \in \mathcal{M}^2\) be a continuous square integrable martingale. We define

\begin{align*} L^2(M) = L^2(\Omega \times \mathbb {R}_+, \mathcal{P}, \mathbb {P} \times d[M]) \end{align*}

in which \(\mathcal{P}\) is the predictable \(\sigma \)-algebra and \(d[M]\) is the measure induced by the quadratic variation of \(M\). The norm on that Hilbert space is \(\Vert X \Vert ^2 = \mathbb {E}\left[ \int _0^{\infty } X_t^2 \: d[M]_t \right]\) .

TODO the sources don’t use the same assumptions: predictable vs progressive (MeasureTheory.ProgMeasurable). Progressive would be more general.

Let \(M \in \mathcal{M}^2\). Then the set of simple processes is dense in \(L^2(M)\).

Proof
Definition 9.26 Itô isometry

Let \(M \in \mathcal{M}^2\). Then the elementary stochastic integral map \(\mathcal{E} \to \mathcal{M}^2\) defined by \(V \mapsto V \cdot M\) extends to an isometry \(L^2(M) \to \mathcal{M}^2\).

Lemma 9.27

\(\langle X \cdot M, Y \cdot M \rangle _{\mathcal{M}^2} = (XY) \cdot \langle M, N \rangle _{\mathcal{M}^2}\).

Proof

9.5.2 Local martingales

Definition 9.28 \(L^2_{loc}(M)\)

Let \(M\) be a continuous local martingale. We define \(L^2_{loc}(M)\) as the space of predictable processes \(X\) such that for all \(t \ge 0\), \(\mathbb {E}\left[ \int _0^t X_s^2 \: d[M]_s \right] {\lt} \infty \).

Definition 9.29 Stochastic integral for continuous local martingales

Let \(M\) be a continuous local martingale and let \(X \in L^2_{loc}(M)\). We define the local stochastic integral \(X \cdot M\) as the unique continuous local martingale with \((X \cdot M)_0 = 0\) such that for any continuous local martingale \(N\), almost surely,

\begin{align*} [X \cdot M, N] = X \cdot [M, N] \: . \end{align*}

9.5.3 Semi-martingales

Definition 9.30

For a continuous semi-martingale \(X = M + A\) and \(V \in L^2_{semi}(X)\) (to be defined) we define the stochastic integral as

\begin{align*} V \cdot X = V \cdot M + V \cdot A \: , \end{align*}

in which \(V \cdot M\) is the local stochastic integral defined in 9.29 and \(V \cdot A\) is the Lebesgue-Stieltjes integral with respect to the locally finite variation process \(A\).

For \(X = M + A\) and \(Y = N + B\), we define the covariation as

\begin{align*} [X, Y] = [M, N] \: . \end{align*}

9.6 Itô formula

Theorem 9.31 Integration by parts

Let \(X\) and \(Y\) be two continuous semi-martingales. Then we have almost surely

\begin{align*} X_t Y_t - X_0 Y_0 = (X \cdot Y)_t + (Y \cdot X)_t + [X,Y]_t \: . \end{align*}
Proof
Theorem 9.32 Itô’s formula

Let \(X^1, \ldots , X^d\) be continuous semi-martingales and let \(f : \mathbb {R}^d \to \mathbb {R}\) be a twice continuously differentiable function. Then, writing \(X = (X^1, \ldots , X^d)\), the process \(f(X)\) is a semi-martingale and we have

\begin{align*} f(X_t) & = f(X_0) + \sum _{i=1}^d \int _0^t \frac{\partial f}{\partial x_i}(X_s) \: dX^i_s + \frac{1}{2} \sum _{i,j=1}^d \int _0^t \frac{\partial ^2 f}{\partial x_i \partial x_j}(X_s) \: d[X^i, X^j]_s \: . \end{align*}
Proof