Documentation

Mathlib.Probability.Martingale.Convergence

Martingale convergence theorems #

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.

Implementationwise, we have tendsto_of_no_upcrossings which shows 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 introduce Filtration.limitProcess which chooses the limiting random variable of a stochastic process if it exists, otherwise returning 0. Hence, instead of showing an existence statement, we phrase the a.e. martingale convergence theorem by showing that a submartingale converges to its limitProcess almost everywhere.

theorem MeasureTheory.not_frequently_of_upcrossings_lt_top {Ω : Type u_1} {a : } {b : } {f : Ω} {ω : Ω} (hab : a < b) (hω : MeasureTheory.upcrossings a b f ω ) :
¬((∃ᶠ (n : ) in Filter.atTop, f n ω < a) ∃ᶠ (n : ) in Filter.atTop, 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 MeasureTheory.upcrossings_eq_top_of_frequently_lt {Ω : Type u_1} {a : } {b : } {f : Ω} {ω : Ω} (hab : a < b) (h₁ : ∃ᶠ (n : ) in Filter.atTop, f n ω < a) (h₂ : ∃ᶠ (n : ) in Filter.atTop, b < f n ω) :

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

theorem MeasureTheory.tendsto_of_uncrossing_lt_top {Ω : Type u_1} {f : Ω} {ω : Ω} (hf₁ : Filter.liminf (fun (n : ) => f n ω‖₊) Filter.atTop < ) (hf₂ : ∀ (a b : ), a < bMeasureTheory.upcrossings (↑a) (↑b) f ω < ) :
∃ (c : ), Filter.Tendsto (fun (n : ) => f n ω) Filter.atTop (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 MeasureTheory.Submartingale.upcrossings_ae_lt_top' {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} {a : } {b : } {f : Ω} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f μ) (hbdd : ∀ (n : ), MeasureTheory.eLpNorm (f n) 1 μ R) (hab : a < b) :
∀ᵐ (ω : Ω) ∂μ, MeasureTheory.upcrossings a b f ω <

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

theorem MeasureTheory.Submartingale.upcrossings_ae_lt_top {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} {f : Ω} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f μ) (hbdd : ∀ (n : ), MeasureTheory.eLpNorm (f n) 1 μ R) :
∀ᵐ (ω : Ω) ∂μ, ∀ (a b : ), a < bMeasureTheory.upcrossings (↑a) (↑b) f ω <
theorem MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} {f : Ω} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f μ) (hbdd : ∀ (n : ), MeasureTheory.eLpNorm (f n) 1 μ R) :
∀ᵐ (ω : Ω) ∂μ, ∃ (c : ), Filter.Tendsto (fun (n : ) => f n ω) Filter.atTop (nhds c)

An L¹-bounded submartingale converges almost everywhere.

theorem MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} {f : Ω} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f μ) (hbdd : ∀ (n : ), MeasureTheory.eLpNorm (f n) 1 μ R) :
∀ᵐ (ω : Ω) ∂μ.trim , ∃ (c : ), Filter.Tendsto (fun (n : ) => f n ω) Filter.atTop (nhds c)
theorem MeasureTheory.Submartingale.ae_tendsto_limitProcess {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} {f : Ω} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ] (hf : MeasureTheory.Submartingale f μ) (hbdd : ∀ (n : ), MeasureTheory.eLpNorm (f n) 1 μ R) :
∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ) => f n ω) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess f μ ω))

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

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 MeasureTheory.uniformIntegrable_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 sufficiently 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 sufficiently 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 phrase the L¹-martingale convergence theorem by proving that a submartingale does converge in L¹ to its limitProcess. However, in contrast to the a.e. martingale convergence theorem, we do not need to introduce an L¹ version of Filtration.limitProcess as the L¹ limit and the a.e. limit of a submartingale coincide.

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.

@[deprecated MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess]

Alias of MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess.


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 MeasureTheory.Martingale.eq_condexp_of_tendsto_eLpNorm {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration m0} {f : Ω} {g : Ω} {μ : MeasureTheory.Measure Ω} (hf : MeasureTheory.Martingale f μ) (hg : MeasureTheory.Integrable g μ) (hgtends : Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0)) (n : ) :
f n =ᵐ[μ] MeasureTheory.condexp ( 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].

@[deprecated MeasureTheory.Martingale.eq_condexp_of_tendsto_eLpNorm]
theorem MeasureTheory.Martingale.eq_condexp_of_tendsto_snorm {Ω : Type u_1} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration m0} {f : Ω} {g : Ω} {μ : MeasureTheory.Measure Ω} (hf : MeasureTheory.Martingale f μ) (hg : MeasureTheory.Integrable g μ) (hgtends : Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (f n - g) 1 μ) Filter.atTop (nhds 0)) (n : ) :
f n =ᵐ[μ] MeasureTheory.condexp ( n) μ g

Alias of MeasureTheory.Martingale.eq_condexp_of_tendsto_eLpNorm.


If a martingale f adapted to converges in L¹ to g, then for all n, f n is almost everywhere equal to 𝔼[g | ℱ 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 MeasureTheory.Integrable.tendsto_ae_condexp {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {g : Ω} (hg : MeasureTheory.Integrable g μ) (hgmeas : MeasureTheory.StronglyMeasurable g) :
∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun (n : ) => MeasureTheory.condexp ( n) μ g x) Filter.atTop (nhds (g x))

Part c of the L¹ martingale convergence theorem: Given an 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 MeasureTheory.Integrable.tendsto_eLpNorm_condexp

Part c of the L¹ martingale convergence theorem: Given an 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 MeasureTheory.Integrable.tendsto_ae_condexp

@[deprecated MeasureTheory.Integrable.tendsto_eLpNorm_condexp]

Alias of MeasureTheory.Integrable.tendsto_eLpNorm_condexp.


Part c of the L¹ martingale convergence theorem: Given an 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 MeasureTheory.Integrable.tendsto_ae_condexp

theorem MeasureTheory.tendsto_ae_condexp {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] (g : Ω) :
∀ᵐ (x : Ω) ∂μ, Filter.Tendsto (fun (n : ) => MeasureTheory.condexp ( n) μ g x) Filter.atTop (nhds (MeasureTheory.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 MeasureTheory.tendsto_eLpNorm_condexp {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] (g : Ω) :
Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (MeasureTheory.condexp ( n) μ g - MeasureTheory.condexp (⨆ (n : ), n) μ g) 1 μ) Filter.atTop (nhds 0)

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

@[deprecated MeasureTheory.tendsto_eLpNorm_condexp]
theorem MeasureTheory.tendsto_snorm_condexp {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] (g : Ω) :
Filter.Tendsto (fun (n : ) => MeasureTheory.eLpNorm (MeasureTheory.condexp ( n) μ g - MeasureTheory.condexp (⨆ (n : ), n) μ g) 1 μ) Filter.atTop (nhds 0)

Alias of MeasureTheory.tendsto_eLpNorm_condexp.


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