# mathlib3documentation

probability.martingale.convergence

# 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 #

### 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.

theorem measure_theory.not_frequently_of_upcrossings_lt_top {Ω : Type u_1} {a b : } {f : Ω } {ω : Ω} (hab : a < b) (hω : ω ) :
¬((∃ᶠ (n : ) in filter.at_top, f n ω < a) ∃ᶠ (n : ) in filter.at_top, b < f n ω)

If a stochastic process has bounded upcrossing from below a to above b, then it does not frequently visit both below a and above b.

theorem measure_theory.upcrossings_eq_top_of_frequently_lt {Ω : Type u_1} {a b : } {f : Ω } {ω : Ω} (hab : a < b) (h₁ : ∃ᶠ (n : ) in filter.at_top, f n ω < a) (h₂ : ∃ᶠ (n : ) in filter.at_top, b < f n ω) :
ω =

A stochastic process that frequently visits below a and above b have infinite upcrossings.

theorem measure_theory.tendsto_of_uncrossing_lt_top {Ω : Type u_1} {f : Ω } {ω : Ω} (hf₁ : filter.liminf (λ (n : ), f n ω‖₊) filter.at_top < ) (hf₂ : (a b : ), a < b ω < ) :
(c : ), filter.tendsto (λ (n : ), f n ω) filter.at_top (nhds c)

A realization of a stochastic process with bounded upcrossings and bounded liminfs is convergent.

We use the spelling < ∞ instead of the standard ≠ ∞ in the assumptions since it is not as easy to change < to under binders.

theorem measure_theory.submartingale.upcrossings_ae_lt_top' {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {a b : } {f : Ω } {R : nnreal} (hf : μ) (hbdd : (n : ), measure_theory.snorm (f n) 1 μ R) (hab : a < b) :
∀ᵐ (ω : Ω) μ, ω <

An L¹-bounded submartingale has bounded upcrossings almost everywhere.

theorem measure_theory.submartingale.upcrossings_ae_lt_top {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hbdd : (n : ), measure_theory.snorm (f n) 1 μ R) :
∀ᵐ (ω : Ω) μ, (a b : ), a < b ω <
theorem measure_theory.submartingale.exists_ae_tendsto_of_bdd {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hbdd : (n : ), measure_theory.snorm (f n) 1 μ R) :
∀ᵐ (ω : Ω) μ, (c : ), filter.tendsto (λ (n : ), f n ω) filter.at_top (nhds c)

An L¹-bounded submartingale converges almost everywhere.

theorem measure_theory.submartingale.exists_ae_trim_tendsto_of_bdd {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hbdd : (n : ), measure_theory.snorm (f n) 1 μ R) :
∀ᵐ (ω : Ω) μ.trim _, (c : ), filter.tendsto (λ (n : ), f n ω) filter.at_top (nhds c)
theorem measure_theory.submartingale.ae_tendsto_limit_process {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} (hf : μ) (hbdd : (n : ), measure_theory.snorm (f n) 1 μ R) :
∀ᵐ (ω : Ω) μ, filter.tendsto (λ (n : ), f n ω) filter.at_top (nhds ω))

Almost everywhere martingale convergence theorem: An L¹-bounded submartingale converges almost everywhere to a ⨆ n, ℱ n-measurable function.

theorem measure_theory.submartingale.mem_ℒp_limit_process {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } {R : nnreal} {p : ennreal} (hf : μ) (hbdd : (n : ), measure_theory.snorm (f n) p μ R) :

The limiting process of an Lᵖ-bounded submartingale is Lᵖ.

### 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.

theorem measure_theory.submartingale.tendsto_snorm_one_limit_process {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } (hf : μ) (hunif : μ) :
filter.tendsto (λ (n : ), 1 μ) filter.at_top (nhds 0)

Part a of the L¹ martingale convergence theorem: a uniformly integrable submartingale adapted to the filtration converges a.e. and in L¹ to an integrable function which is measurable with respect to the σ-algebra ⨆ n, ℱ n.

theorem measure_theory.submartingale.ae_tendsto_limit_process_of_uniform_integrable {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } (hf : μ) (hunif : μ) :
∀ᵐ (ω : Ω) μ, filter.tendsto (λ (n : ), f n ω) filter.at_top (nhds ω))
theorem measure_theory.martingale.eq_condexp_of_tendsto_snorm {Ω : Type u_1} {m0 : measurable_space Ω} {ℱ : m0} {f : Ω } {g : Ω } {μ : measure_theory.measure Ω} (hf : μ) (hg : μ) (hgtends : filter.tendsto (λ (n : ), measure_theory.snorm (f n - g) 1 μ) filter.at_top (nhds 0)) (n : ) :
f n =ᵐ[μ] μ g

If a martingale f adapted to converges in L¹ to g, then for all n, f n is almost everywhere equal to 𝔼[g | ℱ n].

theorem measure_theory.martingale.ae_eq_condexp_limit_process {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : Ω } (hf : μ) (hbdd : μ) (n : ) :
f n =ᵐ[μ] μ

Part b of the L¹ martingale convergence theorem: if f is a uniformly integrable martingale adapted to the filtration , then for all n, f n is almost everywhere equal to the conditional expectation of its limiting process wrt. ℱ n.

theorem measure_theory.integrable.tendsto_ae_condexp {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {g : Ω } (hg : μ) (hgmeas : measure_theory.strongly_measurable g) :
∀ᵐ (x : Ω) μ, filter.tendsto (λ (n : ), μ g x) filter.at_top (nhds (g x))

Part c of the L¹ martingale convergnce theorem: Given a integrable function g which is measurable with respect to ⨆ n, ℱ n where is a filtration, the martingale defined by 𝔼[g | ℱ n] converges almost everywhere to g.

This martingale also converges to g in L¹ and this result is provided by measure_theory.integrable.tendsto_snorm_condexp

Part c of the L¹ martingale convergnce theorem: Given a integrable function g which is measurable with respect to ⨆ n, ℱ n where is a filtration, the martingale defined by 𝔼[g | ℱ n] converges in L¹ to g.

This martingale also converges to g almost everywhere and this result is provided by measure_theory.integrable.tendsto_ae_condexp

theorem measure_theory.tendsto_ae_condexp {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} (g : Ω ) :
∀ᵐ (x : Ω) μ, filter.tendsto (λ (n : ), μ g x) filter.at_top (nhds (measure_theory.condexp ( (n : ), ℱ n) μ g x))

Lévy's upward theorem, almost everywhere version: given a function g and a filtration , the sequence defined by 𝔼[g | ℱ n] converges almost everywhere to 𝔼[g | ⨆ n, ℱ n].

theorem measure_theory.tendsto_snorm_condexp {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} (g : Ω ) :

Lévy's upward theorem, L¹ version: given a function g and a filtration , the sequence defined by 𝔼[g | ℱ n] converges in L¹ to 𝔼[g | ⨆ n, ℱ n].