|
| 1 | +/- |
| 2 | +Copyright (c) 2022 Kexing Ying. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Kexing Ying |
| 5 | +-/ |
| 6 | +import probability.martingale.upcrossing |
| 7 | +import measure_theory.function.uniform_integrable |
| 8 | +import measure_theory.constructions.polish |
| 9 | + |
| 10 | +/-! |
| 11 | +
|
| 12 | +# Martingale convergence theorems |
| 13 | +
|
| 14 | +The martingale convergence theorems are a collection of theorems characterizing the convergence |
| 15 | +of a martingale provided it satisfies some boundedness conditions. This file contains the |
| 16 | +almost everywhere martingale convergence theorem which provides an almost everywhere limit to |
| 17 | +an L¹ bounded submartingale. |
| 18 | +
|
| 19 | +## Main results |
| 20 | +
|
| 21 | +* `measure_theory.submartingale.ae_tendsto_limit_process`: the almost everywhere martingale |
| 22 | + convergence theorem: an L¹-bounded submartingale adapted to the filtration `ℱ` converges almost |
| 23 | + everywhere to its limit process. |
| 24 | +* `measure_theory.submartingale.mem_ℒ1_limit_process`: the limit process of an L¹-bounded |
| 25 | + submartingale is integrable. |
| 26 | +
|
| 27 | +-/ |
| 28 | + |
| 29 | +open topological_space filter measure_theory.filtration |
| 30 | +open_locale nnreal ennreal measure_theory probability_theory big_operators topological_space |
| 31 | + |
| 32 | +namespace measure_theory |
| 33 | + |
| 34 | +variables {Ω ι : Type*} {m0 : measurable_space Ω} {μ : measure Ω} {ℱ : filtration ℕ m0} |
| 35 | +variables {a b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω} {R : ℝ≥0} |
| 36 | + |
| 37 | +section ae_convergence |
| 38 | + |
| 39 | +/-! |
| 40 | +
|
| 41 | +### Almost everywhere martingale convergence theorem |
| 42 | +
|
| 43 | +We will now prove the almost everywhere martingale convergence theorem. |
| 44 | +
|
| 45 | +The a.e. martingale convergence theorem states: if `f` is an L¹-bounded `ℱ`-submartingale, then |
| 46 | +it converges almost everywhere to an integrable function which is measurable with respect to |
| 47 | +the σ-algebra `ℱ∞ := ⨆ n, ℱ n`. |
| 48 | +
|
| 49 | +Mathematically, we proceed by first noting that a real sequence $(x_n)$ converges if |
| 50 | +(a) $\limsup_{n \to \infty} |x_n| < \infty$, (b) for all $a < b \in \mathbb{Q}$ we have the |
| 51 | +number of upcrossings of $(x_n)$ from below $a$ to above $b$ is finite. |
| 52 | +Thus, for all $\omega$ satisfying $\limsup_{n \to \infty} |f_n(\omega)| < \infty$ and the number of |
| 53 | +upcrossings of $(f_n(\omega))$ from below $a$ to above $b$ is finite for all $a < b \in \mathbb{Q}$, |
| 54 | +we have $(f_n(\omega))$ is convergent. |
| 55 | +
|
| 56 | +Hence, assuming $(f_n)$ is L¹-bounded, using Fatou's lemma, we have |
| 57 | +$$ |
| 58 | + \mathbb{E] \limsup_{n \to \infty} |f_n| \le \limsup_{n \to \infty} \mathbb{E}|f_n| < \infty |
| 59 | +$$ |
| 60 | +implying $\limsup_{n \to \infty} |f_n| < \infty$ a.e. Furthermore, by the upcrossing estimate, |
| 61 | +the number of upcrossings is finite almost everywhere implying $f$ converges pointwise almost |
| 62 | +everywhere. |
| 63 | +
|
| 64 | +Thus, denoting $g$ the a.e. limit of $(f_n)$, $g$ is $\mathcal{F}_\infty$-measurable as for all |
| 65 | +$n$, $f_n$ is $\mathcal{F}_n$-measurable and $\mathcal{F}_n \le \mathcal{F}_\infty$. Finally, $g$ |
| 66 | +is integrable as $|g| \le \liminf_{n \to \infty} |f_n|$ so |
| 67 | +$$ |
| 68 | + \mathbb{E}|g| \le \mathbb{E} \limsup_{n \to \infty} |f_n| \le |
| 69 | + \limsup_{n \to \infty} \mathbb{E}|f_n| < \infty |
| 70 | +$$ |
| 71 | +as required. |
| 72 | +
|
| 73 | +Implementation wise, we have `tendsto_of_no_upcrossings` which showed that |
| 74 | +a bounded sequence converges if it does not visit below $a$ and above $b$ infinitely often |
| 75 | +for all $a, b ∈ s$ for some dense set $s$. So, we may skip the first step provided we can prove |
| 76 | +that the realizations are bounded almost everywhere. Indeed, suppose $(|f_n(\omega)|)$ is not |
| 77 | +bounded, then either $f_n(\omega) \to \pm \infty$ or one of $\limsup f_n(\omega)$ or |
| 78 | +$\liminf f_n(\omega)$ equals $\pm \infty$ while the other is finite. But the first case |
| 79 | +contradicts $\liminf |f_n(\omega)| < \infty$ while the second case contradicts finite upcrossings. |
| 80 | +
|
| 81 | +-/ |
| 82 | + |
| 83 | +/-- If a stochastic process has bounded upcrossing from below `a` to above `b`, |
| 84 | +then it does not frequently visit both below `a` and above `b`. -/ |
| 85 | +lemma not_frequently_of_upcrossings_lt_top (hab : a < b) (hω : upcrossings a b f ω ≠ ∞) : |
| 86 | + ¬((∃ᶠ n in at_top, f n ω < a) ∧ (∃ᶠ n in at_top, b < f n ω)) := |
| 87 | +begin |
| 88 | + rw [← lt_top_iff_ne_top, upcrossings_lt_top_iff] at hω, |
| 89 | + replace hω : ∃ k, ∀ N, upcrossings_before a b f N ω < k, |
| 90 | + { obtain ⟨k, hk⟩ := hω, |
| 91 | + exact ⟨k + 1, λ N, lt_of_le_of_lt (hk N) k.lt_succ_self⟩ }, |
| 92 | + rintro ⟨h₁, h₂⟩, |
| 93 | + rw frequently_at_top at h₁ h₂, |
| 94 | + refine not_not.2 hω _, |
| 95 | + push_neg, |
| 96 | + intro k, |
| 97 | + induction k with k ih, |
| 98 | + { simp only [zero_le', exists_const] }, |
| 99 | + { obtain ⟨N, hN⟩ := ih, |
| 100 | + obtain ⟨N₁, hN₁, hN₁'⟩ := h₁ N, |
| 101 | + obtain ⟨N₂, hN₂, hN₂'⟩ := h₂ N₁, |
| 102 | + exact ⟨(N₂ + 1), nat.succ_le_of_lt $ lt_of_le_of_lt hN |
| 103 | + (upcrossings_before_lt_of_exists_upcrossing hab hN₁ hN₁' hN₂ hN₂')⟩ } |
| 104 | +end |
| 105 | + |
| 106 | +/-- A stochastic process that frequently visits below `a` and above `b` have infinite |
| 107 | +upcrossings. -/ |
| 108 | +lemma upcrossings_eq_top_of_frequently_lt (hab : a < b) |
| 109 | + (h₁ : ∃ᶠ n in at_top, f n ω < a) (h₂ : ∃ᶠ n in at_top, b < f n ω) : |
| 110 | + upcrossings a b f ω = ∞ := |
| 111 | +classical.by_contradiction (λ h, not_frequently_of_upcrossings_lt_top hab h ⟨h₁, h₂⟩) |
| 112 | + |
| 113 | +/-- A realization of a stochastic process with bounded upcrossings and bounded liminfs is |
| 114 | +convergent. |
| 115 | +
|
| 116 | +We use the spelling `< ∞` instead of the standard `≠ ∞` in the assumptions since it is not as easy |
| 117 | +to change `<` to `≠` under binders. -/ |
| 118 | +lemma tendsto_of_uncrossing_lt_top |
| 119 | + (hf₁ : liminf at_top (λ n, (∥f n ω∥₊ : ℝ≥0∞)) < ∞) |
| 120 | + (hf₂ : ∀ a b : ℚ, a < b → upcrossings a b f ω < ∞) : |
| 121 | + ∃ c, tendsto (λ n, f n ω) at_top (𝓝 c) := |
| 122 | +begin |
| 123 | + by_cases h : is_bounded_under (≤) at_top (λ n, |f n ω|), |
| 124 | + { rw is_bounded_under_le_abs at h, |
| 125 | + refine tendsto_of_no_upcrossings rat.dense_range_cast _ h.1 h.2, |
| 126 | + { intros a ha b hb hab, |
| 127 | + obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := ⟨ha, hb⟩, |
| 128 | + exact not_frequently_of_upcrossings_lt_top hab (hf₂ a b (rat.cast_lt.1 hab)).ne } }, |
| 129 | + { obtain ⟨a, b, hab, h₁, h₂⟩ := ennreal.exists_upcrossings_of_not_bounded_under hf₁.ne h, |
| 130 | + exact false.elim ((hf₂ a b hab).ne |
| 131 | + (upcrossings_eq_top_of_frequently_lt (rat.cast_lt.2 hab) h₁ h₂)) } |
| 132 | +end |
| 133 | + |
| 134 | +/-- An L¹-bounded submartingale has bounded upcrossings almost everywhere. -/ |
| 135 | +lemma submartingale.upcrossings_ae_lt_top' [is_finite_measure μ] |
| 136 | + (hf : submartingale f ℱ μ) (hbdd : ∀ n, snorm (f n) 1 μ ≤ R) (hab : a < b) : |
| 137 | + ∀ᵐ ω ∂μ, upcrossings a b f ω < ∞ := |
| 138 | +begin |
| 139 | + refine ae_lt_top (hf.adapted.measurable_upcrossings hab) _, |
| 140 | + have := hf.mul_lintegral_upcrossings_le_lintegral_pos_part a b, |
| 141 | + rw [mul_comm, ← ennreal.le_div_iff_mul_le] at this, |
| 142 | + { refine (lt_of_le_of_lt this (ennreal.div_lt_top _ _)).ne, |
| 143 | + { have hR' : ∀ n, ∫⁻ ω, ∥f n ω - a∥₊ ∂μ ≤ R + ∥a∥₊ * μ set.univ, |
| 144 | + { simp_rw snorm_one_eq_lintegral_nnnorm at hbdd, |
| 145 | + intro n, |
| 146 | + refine (lintegral_mono _ : ∫⁻ ω, ∥f n ω - a∥₊ ∂μ ≤ ∫⁻ ω, ∥f n ω∥₊ + ∥a∥₊ ∂μ).trans _, |
| 147 | + { intro ω, |
| 148 | + simp_rw [sub_eq_add_neg, ← nnnorm_neg a, ← ennreal.coe_add, ennreal.coe_le_coe], |
| 149 | + exact nnnorm_add_le _ _ }, |
| 150 | + { simp_rw [ lintegral_add_right _ measurable_const, lintegral_const], |
| 151 | + exact add_le_add (hbdd _) le_rfl } }, |
| 152 | + refine ne_of_lt (supr_lt_iff.2 ⟨R + ∥a∥₊ * μ set.univ, ennreal.add_lt_top.2 |
| 153 | + ⟨ennreal.coe_lt_top, ennreal.mul_lt_top ennreal.coe_lt_top.ne (measure_ne_top _ _)⟩, |
| 154 | + λ n, le_trans _ (hR' n)⟩), |
| 155 | + refine lintegral_mono (λ ω, _), |
| 156 | + rw [ennreal.of_real_le_iff_le_to_real, ennreal.coe_to_real, coe_nnnorm], |
| 157 | + by_cases hnonneg : 0 ≤ f n ω - a, |
| 158 | + { rw [lattice_ordered_comm_group.pos_of_nonneg _ hnonneg, |
| 159 | + real.norm_eq_abs, abs_of_nonneg hnonneg] }, |
| 160 | + { rw lattice_ordered_comm_group.pos_of_nonpos _ (not_le.1 hnonneg).le, |
| 161 | + exact norm_nonneg _ }, |
| 162 | + { simp only [ne.def, ennreal.coe_ne_top, not_false_iff] } }, |
| 163 | + { simp only [hab, ne.def, ennreal.of_real_eq_zero, sub_nonpos, not_le] } }, |
| 164 | + { simp only [hab, ne.def, ennreal.of_real_eq_zero, sub_nonpos, not_le, true_or]}, |
| 165 | + { simp only [ne.def, ennreal.of_real_ne_top, not_false_iff, true_or] } |
| 166 | +end |
| 167 | + |
| 168 | +lemma submartingale.upcrossings_ae_lt_top [is_finite_measure μ] |
| 169 | + (hf : submartingale f ℱ μ) (hbdd : ∀ n, snorm (f n) 1 μ ≤ R) : |
| 170 | + ∀ᵐ ω ∂μ, ∀ a b : ℚ, a < b → upcrossings a b f ω < ∞ := |
| 171 | +begin |
| 172 | + simp only [ae_all_iff, eventually_imp_distrib_left], |
| 173 | + rintro a b hab, |
| 174 | + exact hf.upcrossings_ae_lt_top' hbdd (rat.cast_lt.2 hab), |
| 175 | +end |
| 176 | + |
| 177 | +/-- An L¹-bounded submartingale converges almost everywhere. -/ |
| 178 | +lemma submartingale.exists_ae_tendsto_of_bdd [is_finite_measure μ] |
| 179 | + (hf : submartingale f ℱ μ) (hbdd : ∀ n, snorm (f n) 1 μ ≤ R) : |
| 180 | + ∀ᵐ ω ∂μ, ∃ c, tendsto (λ n, f n ω) at_top (𝓝 c) := |
| 181 | +begin |
| 182 | + filter_upwards [hf.upcrossings_ae_lt_top hbdd, ae_bdd_liminf_at_top_of_snorm_bdd one_ne_zero |
| 183 | + (λ n, (hf.strongly_measurable n).measurable.mono (ℱ.le n) le_rfl) hbdd] with ω h₁ h₂, |
| 184 | + exact tendsto_of_uncrossing_lt_top h₂ h₁, |
| 185 | +end |
| 186 | + |
| 187 | +lemma submartingale.exists_ae_trim_tendsto_of_bdd [is_finite_measure μ] |
| 188 | + (hf : submartingale f ℱ μ) (hbdd : ∀ n, snorm (f n) 1 μ ≤ R) : |
| 189 | + ∀ᵐ ω ∂(μ.trim (Sup_le (λ m ⟨n, hn⟩, hn ▸ ℱ.le _) : (⨆ n, ℱ n) ≤ m0)), |
| 190 | + ∃ c, tendsto (λ n, f n ω) at_top (𝓝 c) := |
| 191 | +begin |
| 192 | + rw [ae_iff, trim_measurable_set_eq], |
| 193 | + { exact hf.exists_ae_tendsto_of_bdd hbdd }, |
| 194 | + { exact measurable_set.compl (@measurable_set_exists_tendsto _ _ _ _ _ _ (⨆ n, ℱ n) _ _ _ _ _ |
| 195 | + (λ n, ((hf.strongly_measurable n).measurable.mono (le_Sup ⟨n, rfl⟩) le_rfl))) } |
| 196 | +end |
| 197 | + |
| 198 | +/-- **Almost everywhere martingale convergence theorem**: An L¹-bounded submartingale converges |
| 199 | +almost everywhere to a `⨆ n, ℱ n`-measurable function. -/ |
| 200 | +lemma submartingale.ae_tendsto_limit_process [is_finite_measure μ] |
| 201 | + (hf : submartingale f ℱ μ) (hbdd : ∀ n, snorm (f n) 1 μ ≤ R) : |
| 202 | + ∀ᵐ ω ∂μ, tendsto (λ n, f n ω) at_top (𝓝 (ℱ.limit_process f μ ω)) := |
| 203 | +begin |
| 204 | + classical, |
| 205 | + suffices : ∃ g, strongly_measurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, tendsto (λ n, f n ω) at_top (𝓝 (g ω)), |
| 206 | + { rw [limit_process, dif_pos this], |
| 207 | + exact (classical.some_spec this).2 }, |
| 208 | + set g' : Ω → ℝ := λ ω, if h : ∃ c, tendsto (λ n, f n ω) at_top (𝓝 c) then h.some else 0, |
| 209 | + have hle : (⨆ n, ℱ n) ≤ m0 := Sup_le (λ m ⟨n, hn⟩, hn ▸ ℱ.le _), |
| 210 | + have hg' : ∀ᵐ ω ∂(μ.trim hle), tendsto (λ n, f n ω) at_top (𝓝 (g' ω)), |
| 211 | + { filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω, |
| 212 | + simp_rw [g', dif_pos hω], |
| 213 | + exact hω.some_spec }, |
| 214 | + have hg'm : @ae_strongly_measurable _ _ _ (⨆ n, ℱ n) g' (μ.trim hle) := |
| 215 | + (@ae_measurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _ |
| 216 | + (λ n, ((hf.strongly_measurable n).measurable.mono |
| 217 | + (le_Sup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n) le_rfl).ae_measurable) hg').ae_strongly_measurable, |
| 218 | + obtain ⟨g, hgm, hae⟩ := hg'm, |
| 219 | + have hg : ∀ᵐ ω ∂μ.trim hle, tendsto (λ n, f n ω) at_top (𝓝 (g ω)), |
| 220 | + { filter_upwards [hae, hg'] with ω hω hg'ω, |
| 221 | + exact hω ▸ hg'ω }, |
| 222 | + exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩, |
| 223 | +end |
| 224 | + |
| 225 | +/-- The limiting process of an Lᵖ-bounded submartingale is Lᵖ. -/ |
| 226 | +lemma submartingale.mem_ℒp_limit_process {p : ℝ≥0∞} |
| 227 | + (hf : submartingale f ℱ μ) (hbdd : ∀ n, snorm (f n) p μ ≤ R) : |
| 228 | + mem_ℒp (ℱ.limit_process f μ) p μ := |
| 229 | +mem_ℒp_limit_process_of_snorm_bdd |
| 230 | + (λ n, ((hf.strongly_measurable n).mono (ℱ.le n)).ae_strongly_measurable) hbdd |
| 231 | + |
| 232 | +end ae_convergence |
| 233 | + |
| 234 | +end measure_theory |
0 commit comments