Martingale convergence theorems #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The martingale convergence theorems are a collection of theorems characterizing the convergence of a martingale provided it satisfies some boundedness conditions. This file contains the almost everywhere martingale convergence theorem which provides an almost everywhere limit to an L¹ bounded submartingale. It also contains the L¹ martingale convergence theorem which provides an L¹ limit to a uniformly integrable submartingale. Finally, it also contains the Lévy upwards theorems.

Main results #

• measure_theory.submartingale.ae_tendsto_limit_process: the almost everywhere martingale convergence theorem: an L¹-bounded submartingale adapted to the filtration ℱ converges almost everywhere to its limit process.
• measure_theory.submartingale.mem_ℒp_limit_process: the limit process of an Lᵖ-bounded submartingale is Lᵖ.
• measure_theory.submartingale.tendsto_snorm_one_limit_process: part a of the L¹ martingale convergence theorem: a uniformly integrable submartingale adapted to the filtration ℱ converges almost everywhere and in L¹ to an integrable function which is measurable with respect to the σ-algebra ⨆ n, ℱ n.
• measure_theory.martingale.ae_eq_condexp_limit_process: part b the L¹ martingale convergence theorem: if f is a uniformly integrable martingale adapted to the filtration ℱ, then f n equals 𝔼[g | ℱ n] almost everywhere where g is the limiting process of f.
• measure_theory.integrable.tendsto_ae_condexp: part c the L¹ martingale convergence theorem: given a ⨆ n, ℱ n-measurable function g where ℱ is a filtration, 𝔼[g | ℱ n] converges almost everywhere to g.
• measure_theory.integrable.tendsto_snorm_condexp: part c the L¹ martingale convergence theorem: given a ⨆ n, ℱ n-measurable function g where ℱ is a filtration, 𝔼[g | ℱ n] converges in L¹ to g.

Almost everywhere martingale convergence theorem #

We will now prove the almost everywhere martingale convergence theorem.

The a.e. martingale convergence theorem states: if f is an L¹-bounded ℱ-submartingale, then it converges almost everywhere to an integrable function which is measurable with respect to the σ-algebra ℱ∞ := ⨆ n, ℱ n.

Mathematically, we proceed by first noting that a real sequence $(x_n)$ converges if (a) $\limsup_{n \to \infty} |x_n| < \infty$, (b) for all $a < b \in \mathbb{Q}$ we have the number of upcrossings of $(x_n)$ from below $a$ to above $b$ is finite. Thus, for all $\omega$ satisfying $\limsup_{n \to \infty} |f_n(\omega)| < \infty$ and the number of upcrossings of $(f_n(\omega))$ from below $a$ to above $b$ is finite for all $a < b \in \mathbb{Q}$, we have $(f_n(\omega))$ is convergent.

Hence, assuming $(f_n)$ is L¹-bounded, using Fatou's lemma, we have $$ \mathbb{E} \limsup_{n \to \infty} |f_n| \le \limsup_{n \to \infty} \mathbb{E}|f_n| < \infty $$ implying $\limsup_{n \to \infty} |f_n| < \infty$ a.e. Furthermore, by the upcrossing estimate, the number of upcrossings is finite almost everywhere implying $f$ converges pointwise almost everywhere.

Thus, denoting $g$ the a.e. limit of $(f_n)$, $g$ is $\mathcal{F}_\infty$-measurable as for all $n$, $f_n$ is $\mathcal{F}_n$-measurable and $\mathcal{F}_n \le \mathcal{F}_\infty$. Finally, $g$ is integrable as $|g| \le \liminf_{n \to \infty} |f_n|$ so $$ \mathbb{E}|g| \le \mathbb{E} \limsup_{n \to \infty} |f_n| \le \limsup_{n \to \infty} \mathbb{E}|f_n| < \infty $$ as required.

Implementation wise, we have tendsto_of_no_upcrossings which showed that a bounded sequence converges if it does not visit below $a$ and above $b$ infinitely often for all $a, b ∈ s$ for some dense set $s$. So, we may skip the first step provided we can prove that the realizations are bounded almost everywhere. Indeed, suppose $(|f_n(\omega)|)$ is not bounded, then either $f_n(\omega) \to \pm \infty$ or one of $\limsup f_n(\omega)$ or $\liminf f_n(\omega)$ equals $\pm \infty$ while the other is finite. But the first case contradicts $\liminf |f_n(\omega)| < \infty$ while the second case contradicts finite upcrossings.

Furthermore, we introduced filtration.limit_process which chooses the limiting random variable of a stochastic process if it exists, otherwise it returns 0. Hence, instead of showing an existence statement, we phrased the a.e. martingale convergence theorem by showed that a submartingale converges to its limit_process almost everywhere.

L¹ martingale convergence theorem #

We will now prove the L¹ martingale convergence theorems.

The L¹ martingale convergence theorem states that: (a) if f is a uniformly integrable (in the probability sense) submartingale adapted to the filtration ℱ, it converges in L¹ to an integrable function g which is measurable with respect to ℱ∞ := ⨆ n, ℱ n and (b) if f is actually a martingale, f n = 𝔼[g | ℱ n] almost everywhere. (c) Finally, if h is integrable and measurable with respect to ℱ∞, (𝔼[h | ℱ n])ₙ is a uniformly integrable martingale which converges to h almost everywhere and in L¹.

The proof is quite simple. (a) follows directly from the a.e. martingale convergence theorem and the Vitali convergence theorem as our definition of uniform integrability (in the probability sense) directly implies L¹-uniform boundedness. We note that our definition of uniform integrability is slightly non-standard but is equivalent to the usual literary definition. This equivalence is provided by measure_theory.uniform_integrable_iff.

(b) follows since given $n$, we have for all $m \ge n$, $$ \|f_n - \mathbb{E}[g \mid \mathcal{F}_n]\|_1 = \|\mathbb{E}[f_m - g \mid \mathcal{F}_n]\|_1 \le \|\|f_m - g\|_1. $$ Thus, taking $m \to \infty$ provides the almost everywhere equality.

Finally, to prove (c), we define $f_n := \mathbb{E}[h \mid \mathcal{F}_n]$. It is clear that $(f_n)_n$ is a martingale by the tower property for conditional expectations. Furthermore, $(f_n)_n$ is uniformly integrable in the probability sense. Indeed, as a single function is uniformly integrable in the measure theory sense, for all $\epsilon > 0$, there exists some $\delta > 0$ such that for all measurable set $A$ with $\mu(A) < δ$, we have $\mathbb{E}|h|\mathbf{1}_A < \epsilon$. So, since for sufficently large $\lambda$, by the Markov inequality, we have for all $n$, $$ \mu(|f_n| \ge \lambda) \le \lambda^{-1}\mathbb{E}|f_n| \le \lambda^{-1}\mathbb|g| < \delta, $$ we have for sufficently large $\lambda$, for all $n$, $$ \mathbb{E}|f_n|\mathbf{1}_{|f_n| \ge \lambda} \le \mathbb|g|\mathbf{1}_{|f_n| \ge \lambda} < \epsilon, $$ implying $(f_n)_n$ is uniformly integrable. Now, to prove $f_n \to h$ almost everywhere and in L¹, it suffices to show that $h = g$ almost everywhere where $g$ is the almost everywhere and L¹ limit of $(f_n)_n$ from part (b) of the theorem. By noting that, for all $s \in \mathcal{F}_n$, we have $$ \mathbb{E}g\mathbf{1}_s = \mathbb{E}[\mathbb{E}[g \mid \mathcal{F}_n]\mathbf{1}_s] = \mathbb{E}[\mathbb{E}[h \mid \mathcal{F}_n]\mathbf{1}_s] = \mathbb{E}h\mathbf{1}_s $$ where $\mathbb{E}[g \mid \mathcal{F}_n = \mathbb{E}[h \mid \mathcal{F}_n]$ almost everywhere by part (b); the equality also holds for all $s \in \mathcal{F}_\infty$ by Dynkin's theorem. Thus, as both $h$ and $g$ are $\mathcal{F}_\infty$-measurable, $h = g$ almost everywhere as required.

Similar to the a.e. martingale convergence theorem, rather than showing the existence of the limiting process, we phrased the L¹-martingale convergence theorem by proving that a submartingale does converge in L¹ to its limit_process. However, in contrast to the a.e. martingale convergence theorem, we do not need to introduce a L¹ version of filtration.limit_process as the L¹ limit and the a.e. limit of a submartingale coincide.