The uniqueness of \(\lambda _X\) is guaranteed by Lemma 13.11, since the predictable rectangles form a semi-ring of sets (Lemma 10.10), one that generates the ring of elementary predictable sets (Lemma 10.13).

This follows (by triangle inequality and additivity of the content) from the Definition 13.14, and from the Lemmata 10.3, 10.7.

By Lemma 10.20, the process \(\mathbb {1}_A\) is a simple one,

where \((s_i, t_i]\) may be taken to be pairwise disjoint, thanks to the Lemma 10.17. Then

taking into account that for all \(i\) we have \(t\wedge t_i = t_i\), \(t\wedge s_i = s_i\), as \(A\subseteq (0, t] \times \Omega \) .

The above boundedness condition,

does not change after restricting the above supremum to sets \(A\) contained in \((0, t] \times \Omega \), since by Lemma 10.37,

Moreover, for those \(A\) the Lemma 13.18 is applicable; in effect, we can express the boundedness condition as

Let \(\mathcal{A}\) be the class of predictable rectangles, and let us use it in the definition of bounded variation of \(\lambda _X\) (see Lemma 13.16).

Fix \(t\in T\) . We aim to show that

holds if and only if

Take an elementary predictable \(A\subset B:=(0,t]\times \Omega \); choose \(A_1\), …, \(A_m\in \mathcal{A}\) to be pairwise disjoint and such that (Corollary 10.8)

Express \(A\) as a disjoint union of some \(A_{m+1}\), …, \(A_n\in \mathcal{A}\) (Lemma 10.14). Clearly, \((A_i)_{i=1}^n\) is a finite \(\mathcal{A}\)-partition of \(B=(0,t]\times \Omega \), so, by content’s additivity,

This shows the "only if" part.

For the "if" direction, take a sequence \(((A_i^k)_{i=1}^{n_k})_{k=1}^\infty \) of finite \(\mathcal{A}\)-partitions of \((0,t]\times \Omega \) such that

Let

and note that \(A_k = \bigcup _{i\in J_k} A_i^k\) is an elementary predictable subset of \((0,t]\times \Omega \) . Without loss of generality, we may assume that

which by additivity means

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

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

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

By Lemma 13.25, \(\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.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.32, 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.42, 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 ) \mathbb {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.59 to \(X - Y\) .

By Lemma 10.41, 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.30, it is enough to show that \(A\) is a local martingale. We have by Lemma 13.61 that \(A\) is a martingale, and hence a local martingale (Lemma 9.27).

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.59 . This is proved in Lemma 13.62 .

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.