Formalization of a Brownian motion and of stochastic integrals in Lean

14 Quasimartingales and measures derived from processes

14.1 Content of a process

Definition 14.1 Additive content
#

Let \(E\) be a commutative monoid and \(\mathcal{A}\) be a family of sets. An additive content is a set function \(\lambda : \mathcal{A} \to E\) with value \(0\) at the empty set which is finitely additive on \(\mathcal{A}\) .

Let \(\lambda \) be an additive content on a semi-ring of sets \(C\) . Then \(\lambda \) admits a unique additive extension to the ring of sets generated by \(C\) .

Proof
Definition 14.3 Content associated with a process

Let \(X : T \to \Omega \to E\), where \(E\) is a Banach space, be an adapted process with \(X_t \in L^1\) for every \(t \in T\) . The content \(\lambda _X\) associated with \(X\) is an \(E\)-valued additive content on elementary predictable sets, given on predictable rectangles by

\begin{align*} \lambda _X((s, t] \times F) & = \mathbb {E}[\mathbb {1}_F (X_t - X_s)], & s {\lt} t \text{ in } T,\ F \in \mathcal{F}_s, \\ \lambda _X(\{ 0\} \times F) & = 0, & F \in \mathcal{F}_0 \: . \end{align*}

The content \(\lambda _X\) associated with \(X\) is uniquely defined.

Proof

The uniqueness of \(\lambda _X\) is guaranteed by Lemma 14.2, 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).

Definition 14.5 Partition of a set
#

An partition of a set \(A\) is a family of pairwise disjoint sets, which does not contain the empty set, and whose union is \(A\) . For a family of sets \(C\), a \(C\)-partition of \(A\) is a partition of \(A\) consisting of sets in \(C\) .

Definition 14.6 Bounded variation of a content

An additive content \(\lambda \) on a ring \(\mathcal{A}\) of sets, with values in a normed space \(E\), has bounded variation on a set \(A \in \mathcal{A}\) if

\begin{align*} \vert \lambda \vert (A) := \sup \Big\{ \sum _{i=1}^n \| \lambda (A_i) \| \: \Big|\: (A_i)_{i=1}^n \text{ finite } \mathcal{A}\text{-partition of } A \Big\} {\lt} \infty \: . \end{align*}

We can equivalently take supremum over \(C\)-partitions of \(A\) in the above definition, when \(\mathcal{A}\) is generated by the semi-ring \(C\) .

Proof

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

The content \(\lambda _X\) associated with a process \(X\) satisfies, for every elementary predictable set \(A\subseteq (0, t] \times \Omega \),

\begin{align*} \lambda _X(A) = \mathbb {E}[(\mathbb {1}_A \bullet X)_t] \: . \end{align*}
Proof

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

\begin{align*} (\mathbb {1}_A)_t = \mathbb {1}_{F_0}\mathbb {1}_{\{ 0\} }(t) + \sum _{i=1}^n \mathbb {1}_{F_i} \mathbb {1}_{(s_i, t_i]}(t) \: , \end{align*}

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

\begin{align*} \mathbb {E}[(\mathbb {1}_A \bullet X)_t] & = \mathbb {E}\left[\sum _{i=1}^n \mathbb {1}_{F_i} (X_{t \wedge t_i} - X_{t \wedge s_i})\right] \\ & = \sum _{i=1}^n \mathbb {E}\left[\mathbb {1}_{F_i} (X_{t \wedge t_i} - X_{t \wedge s_i})\right] \\ & = \sum _{i=1}^n \lambda _X((s_i, t_i] \times F_i) = \lambda _X(A), \end{align*}

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

14.2 Quasi-martingales

Definition 14.9 Quasi-martingale

Let \(E\) be a Banach space. An adapted integrable process \(X : T \to \Omega \to E\) is called a quasi-martingale if the additive content \(\lambda _X\) (on elementary predictable sets) associated with \(X\) has bounded variation on every set \((0, t] \times \Omega \) with \(t \in T\) , that is,

\begin{align*} \forall t \in T, \quad \vert \lambda _X \vert \big((0, t] \times \Omega \big) {\lt} \infty \: . \end{align*}
Lemma 14.10

The content \(\lambda _X\) associated with a real-valued process \(X\) has bounded variation on \((0, t] \times \Omega \) if and only if the set \(\{ \mathbb {E}[(\mathbb {1}_A \bullet X)_t] \mid A \text{ elementary predictable}\} \) is bounded. In particular, an adapted integrable process \(X : T \to \Omega \to \mathbb {R}\) satisfies the conditions of Theorem 11.17, iff it is a quasi-martingale.

Proof

The above boundedness condition,

\[ \sup \Big\{ |\mathbb {E}[(\mathbb {1}_A \bullet X)_t]| \: \Big|\: A \text{ elementary predictable} \Big\} {\lt}\infty \quad \text{for all } t\in T, \]

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

\[ (\mathbb {1}_A \bullet X)_t = (\mathbb {1}_A \bullet X)^t_t = ((\mathbb {1}_{[0, t]}\mathbb {1}_A) \bullet X)_t = ((\mathbb {1}_{(0, t]}\mathbb {1}_A) \bullet X)_t \: . \]

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

\[ \sup \Big\{ |\lambda _X(A)| \: \Big|\: A \text{ elementary predictable},\: A\subset (0,t]\times \Omega \Big\} {\lt}\infty \quad \text{for all } t\in T. \]

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 14.7).

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

\[ \vert \lambda _X \vert ((0,t]\times \Omega ) = \sup \Big\{ \sum _{i=1}^n | \lambda _X(A_i)| \: \Big|\: (A_i)_{i=1}^n \text{ finite } \mathcal{A}\text{-partition of } (0,t]\times \Omega \Big\} {\lt}\infty \]

holds if and only if

\[ \sup \Big\{ |\lambda _X(A)| \: \Big|\: A \text{ elementary predictable},\: A\subset (0,t]\times \Omega \Big\} {\lt}\infty . \]

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)

\[ B\setminus A = \bigcup _{j=1}^m A_j. \]

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,

\[ |\lambda _X(A)| = \left| \sum _{i=m+1}^n \lambda _X(A_i) \right| \le \sum _{i=1}^n |\lambda _X(A_i)|. \]

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

\[ \lim _{k\to \infty } \sum _{i=1}^{n_k} | \lambda _X(A_i^k)| =\infty . \]

Let

\[ J_k = \{ i \mid 1\le i\le n_k, \: \lambda _X(A_i^k) {\gt} 0\} , \]

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

\[ \limsup _{k\to \infty } \sum _{i\in J_k} \lambda _X(A_i^k) = \infty , \]

which by additivity means

\[ \limsup _{k\to \infty } \lambda _X(A_k) = \infty . \]

14.3 Measure associated with a process

TODO: reorganize and update this section, which should for now be considered a draft.

14.3.1 Monotone processes

Definition 14.11
#

Let \(f : T \to \mathbb {R}\) be a right-continuous monotone function on a conditionally complete linear order \(T\). We denote by \(d_+ f\) the measure on \(T\) defined by \(d_+ f((a, b]) = f(b) - f(a)\) for all \(a, b \in T\) .

Lemma 14.12

Let \(X : T \to \Omega \to \mathbb {R}\) be a right-continuous adapted process which is monotone in the time variable. Then the measure \(d_+ X_\omega \) is measurable in \(\omega \) .

Proof

14.3.2 Bounded variation processes

Definition 14.13

Let \(f : T \to E\) be a function of bounded variation on a suitable order \(T\), with \(E\) a complete normed additive group. Then there exists a signed measure \(df\) on \(T\) defined by \(df((a, b]) = f(b^+) - f(a^+)\) .

Lemma 14.14

Let \(X : T \to \Omega \to E\) be an adapted process which is of bounded variation in the time variable. Then the measure \(dX_\omega \) is measurable in \(\omega \) .

Proof

Denoting by \(\vert df \vert \) the total variation of the measure \(df\) , \(V_f([a, b]) = \vert df \vert ([a, b])\) .

Proof

If \(f : T \to \mathbb {R}\) is a right-continuous monotone function, then the measure \(df\) coincides with the measure \(d_+ f\) .

Proof

14.3.3 Integrable processes

Integrable -> content on the ring of sets generated by predictable rectangles. Can be extended to a measure on the predictable \(\sigma \)-algebra if the process is of class DL and ... (see Metivier, Semimartingales, 13.3).

Let \(X : T \to \Omega \to E\) be a stochastic process such that \(X_t\) is integrable for all \(t\) . For \(s {\lt} t\) and \(A \in \mathcal{F}_s\), let

\begin{align*} \mu _X((s, t] \times A) = \mathbb {E}[\mathbb {1}_A (X_t - X_s)] \: . \end{align*}

Set \(\mu _X(\{ 0\} \times A) = 0\) . Then \(\mu _X\) is a content on the predictable rectangles, which can be extended to the ring of sets it generates.

TODO: lemmas stating that those 3 coincide whenever they can.