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

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

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

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

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

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\) ,

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\) ,

By Lemma 10.20, \(V \bullet _B M\) is càdlàg, and we know that it is a martingale by Lemma 10.28 . It remains to show that \(\sup _{t \in T} \Vert (V \bullet _B M)_t \Vert _{L^2} {\lt} \infty \) . By Lemma 13.22, 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.

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

The inner product in \(L^2\) spaces is defined as the integral of the pointwise inner products.

A simple process is bounded by definition.

TODO: this proof (and the result of the lemma) assumes that the intervals defining the simple process are disjoint.

Let \(V \in \mathcal{E}_{T, E}\) , with \(V_t(\omega ) = \sum _{k=1}^n \eta _k(\omega ) \mathbf{1}_{(s_k, t_k]}(t)\) .

There are two steps to the proof.

First, in order to make sense of \(\Vert V \Vert _{L^2(M)}\), we define the natural linear map from \(\mathcal{E}\) to \(L^2(M)\) via SimpleProcess.toFun. (Informally, this is identifying \(\mathcal{E}\) as a subset \(\mathcal{E} \subseteq L^2(M)\).) This induces the \(L^2(M)\)-norm on \(\mathcal{E}\), using something like NormedSpace.induced.

Next, we show that integration \(V \mapsto V \bullet M\) is an isometry from \(\mathcal{E}\) with the \(L^2(M)\)-norm, to \(\mathcal{M}^2\). The proof is TODO.

For \(B\) a measurable set of \(\mathbb {R}_+\) and \(\omega \in \Omega \), let \(\nu _\omega (B) = \int _B X_s(\omega ) \: d\langle M \rangle _s(\omega )\) . This is a signed measure on \(\mathbb {R}_+\) . Then if for all \(t\), \(\int _0^t X_s(\omega ) \: d\langle M \rangle _s(\omega ) = 0\) then \(\nu _\omega ([0,t]) = 0\) for all \(t\). Those intervals generate the Borel \(\sigma \)-algebra on \(\mathbb {R}_+\), so \(\nu _\omega \) is the zero measure. Thus, for almost all \(\omega \), \(\nu _\omega \) is the zero measure.

The measure \(\nu _\omega \) is absolutely continuous with respect to the measure \(d\langle M \rangle (\omega )\) , and its Radon-Nikodym derivative is \(X(\omega )\) . Since \(\nu _\omega \) is the zero measure for almost all \(\omega \), we have that \(X(\omega ) = 0\) \(d\langle M \rangle (\omega )\)-almost everywhere for almost all \(\omega \) . Equivalently, \(X = 0\) \((\mathbb {P} \times d\langle M \rangle )\)-almost everywhere.

By linearity of the integral, we have \(\int _0^t (X_s - Y_s) \: d\langle M \rangle _s = 0\) for all \(t \ge 0\) a.s.. Then apply Lemma 13.49 to \(X - Y\) .

By Lemma 10.25, it is enough to show that for any bounded real simple process \(V\), \(\mathbb {E}[(V \bullet A)_\infty ] = 0\) .

\(A_t := \int _0^t X_s \: d\langle M \rangle _s\) is a finite variation process such that \(A_t\) is integrable for all \(t \ge 0\) . By Theorem 9.29, it is enough to show that \(A\) is a local martingale. We have by Lemma 13.51 that \(A\) is a martingale, and hence a local martingale (Lemma 9.26).

Since \(L^2(M)\) is a Hilbert space, it is enough to show that if \(X \in L^2(M)\) is orthogonal to all simple processes, then \(X = 0\) . Let \(X \in L^2(M)\) such that for any simple process \(V\), \(\mathbb {E}\left[ \int _0^{\infty } X_t V_t \: d\langle M \rangle _t \right] = 0\) . Let \(A_t = \int _0^t X_s \: d\langle M \rangle _s\). It suffices to show that \(A = 0\) by Lemma 13.49 . This is proved in Lemma 13.52 .

In Lean, this is stated as: the natural linear map toFun from \(\mathcal{E}\) to \(L^2(M)\) is IsDenseInducing. The Itô isometry is then defined using IsDenseInducing.extend.