From ad88a836ea126a91e37b267fdb8a3071ceb47fc2 Mon Sep 17 00:00:00 2001
From: Kexing Ying <kexing.ying19@imperial.ac.uk>
Date: Mon, 13 Dec 2021 19:31:50 +0000
Subject: [PATCH] feat(probability_theory/martingale): add
 super/sub-martingales (#10710)

---
 .../function/conditional_expectation.lean     |  12 +-
 src/probability_theory/martingale.lean        | 221 +++++++++++++++++-
 2 files changed, 227 insertions(+), 6 deletions(-)

diff --git a/src/measure_theory/function/conditional_expectation.lean b/src/measure_theory/function/conditional_expectation.lean
index fd2fa4714bfd6..7739417ca78b2 100644
--- a/src/measure_theory/function/conditional_expectation.lean
+++ b/src/measure_theory/function/conditional_expectation.lean
@@ -1705,6 +1705,8 @@ end
 lemma integrable_condexp : integrable (μ[f|m,hm]) μ :=
 (integrable_condexp_L1 f).congr (condexp_ae_eq_condexp_L1 f).symm
 
+variable (hm)
+
 /-- The integral of the conditional expectation `μ[f|hm]` over an `m`-measurable set is equal to
 the integral of `f` on that set. -/
 lemma set_integral_condexp (hf : integrable f μ) (hs : measurable_set[m] s) :
@@ -1714,11 +1716,13 @@ begin
   exact set_integral_condexp_L1 hf hs,
 end
 
+variable {hm}
+
 lemma integral_condexp (hf : integrable f μ) : ∫ x, μ[f|m,hm] x ∂μ = ∫ x, f x ∂μ :=
 begin
   suffices : ∫ x in set.univ, μ[f|m,hm] x ∂μ = ∫ x in set.univ, f x ∂μ,
     by { simp_rw integral_univ at this, exact this, },
-  exact set_integral_condexp hf (@measurable_set.univ _ m),
+  exact set_integral_condexp hm hf (@measurable_set.univ _ m),
 end
 
 /-- **Uniqueness of the conditional expectation**
@@ -1734,7 +1738,7 @@ begin
   refine ae_eq_of_forall_set_integral_eq_of_sigma_finite' hm hg_int_finite
     (λ s hs hμs, integrable_condexp.integrable_on) (λ s hs hμs, _) hgm
     (measurable.ae_measurable' measurable_condexp),
-  rw [hg_eq s hs hμs, set_integral_condexp hf hs],
+  rw [hg_eq s hs hμs, set_integral_condexp hm hf hs],
 end
 
 lemma condexp_add (hf : integrable f μ) (hg : integrable g μ) :
@@ -1777,9 +1781,9 @@ begin
     (λ s hs hμs, integrable_condexp.integrable_on) (λ s hs hμs, integrable_condexp.integrable_on)
     _ (measurable.ae_measurable' measurable_condexp) (measurable.ae_measurable' measurable_condexp),
   intros s hs hμs,
-  rw set_integral_condexp integrable_condexp hs,
+  rw set_integral_condexp _ integrable_condexp hs,
   by_cases hf : integrable f μ,
-  { rw [set_integral_condexp hf hs, set_integral_condexp hf (hm₁₂ s hs)], },
+  { rw [set_integral_condexp _ hf hs, set_integral_condexp _ hf (hm₁₂ s hs)], },
   { simp_rw integral_congr_ae (ae_restrict_of_ae (condexp_undef hf)), },
 end
 
diff --git a/src/probability_theory/martingale.lean b/src/probability_theory/martingale.lean
index 4bb1307a1e30a..7e17ef33eb2f1 100644
--- a/src/probability_theory/martingale.lean
+++ b/src/probability_theory/martingale.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rémy Degenne
+Authors: Rémy Degenne, Kexing Ying
 -/
 
 import probability_theory.stopping
@@ -12,13 +12,22 @@ import measure_theory.function.conditional_expectation
 
 A family of functions `f : ι → α → E` is a martingale with respect to a filtration `ℱ` if every
 `f i` is integrable, `f` is adapted with respect to `ℱ` and for all `i ≤ j`,
-`μ[f j | ℱ.le i] =ᵐ[μ] f i`.
+`μ[f j | ℱ.le i] =ᵐ[μ] f i`. On the other hand, `f : ι → α → E` is said to be a supermartingale
+with respect to the filtration `ℱ` if `f i` is integrable, `f` is adapted with resepct to `ℱ`
+and for all `i ≤ j`, `μ[f j | ℱ.le i] ≤ᵐ[μ] f i`. Finally, `f : ι → α → E` is said to be a
+submartingale with respect to the filtration `ℱ` if `f i` is integrable, `f` is adapted with
+resepct to `ℱ` and for all `i ≤ j`, `f i ≤ᵐ[μ] μ[f j | ℱ.le i]`.
+
 The definitions of filtration and adapted can be found in `probability_theory.stopping`.
 
 ### Definitions
 
 * `measure_theory.martingale f ℱ μ`: `f` is a martingale with respect to filtration `ℱ` and
   measure `μ`.
+* `measure_theory.supermartingale f ℱ μ`: `f` is a supermartingale with respect to
+  filtration `ℱ` and measure `μ`.
+* `measure_theory.submartingale f ℱ μ`: `f` is a submartingale with respect to filtration `ℱ` and
+  measure `μ`.
 
 ### Results
 
@@ -44,6 +53,20 @@ def martingale (f : ι → α → E) (ℱ : filtration ι m0) (μ : measure α)
   [sigma_finite_filtration μ ℱ] : Prop :=
 adapted ℱ f ∧ ∀ i j, i ≤ j → μ[f j | ℱ i, ℱ.le i] =ᵐ[μ] f i
 
+/-- A family of integrable functions `f : ι → α → E` is a supermartingale with respect to a
+filtration `ℱ` if `f` is adapted with respect to `ℱ` and for all `i ≤ j`,
+`μ[f j | ℱ.le i] ≤ᵐ[μ] f i`. -/
+def supermartingale [has_le E] (f : ι → α → E) (ℱ : filtration ι m0) (μ : measure α)
+  [sigma_finite_filtration μ ℱ] : Prop :=
+adapted ℱ f ∧ (∀ i j, i ≤ j → μ[f j | ℱ i, ℱ.le i] ≤ᵐ[μ] f i) ∧ ∀ i, integrable (f i) μ
+
+/-- A family of integrable functions `f : ι → α → E` is a submartingale with respect to a
+filtration `ℱ` if `f` is adapted with respect to `ℱ` and for all `i ≤ j`,
+`f i ≤ᵐ[μ] μ[f j | ℱ.le i]`. -/
+def submartingale [has_le E] (f : ι → α → E) (ℱ : filtration ι m0) (μ : measure α)
+  [sigma_finite_filtration μ ℱ] : Prop :=
+adapted ℱ f ∧ (∀ i j, i ≤ j → f i ≤ᵐ[μ] μ[f j | ℱ i, ℱ.le i]) ∧ ∀ i, integrable (f i) μ
+
 variables (E)
 lemma martingale_zero (ℱ : filtration ι m0) (μ : measure α) [sigma_finite_filtration μ ℱ] :
   martingale (0 : ι → α → E) ℱ μ :=
@@ -63,6 +86,17 @@ hf.2 i j hij
 lemma integrable (hf : martingale f ℱ μ) (i : ι) : integrable (f i) μ :=
 integrable_condexp.congr (hf.condexp_ae_eq (le_refl i))
 
+lemma set_integral_eq (hf : martingale f ℱ μ) {i j : ι} (hij : i ≤ j) {s : set α}
+  (hs : measurable_set[ℱ i] s) :
+  ∫ x in s, f i x ∂μ = ∫ x in s, f j x ∂μ :=
+begin
+  rw ← @set_integral_condexp _ _ _ _ _ _ _ _ (ℱ i) m0 _ (ℱ.le i) _ _ _ (hf.integrable j) hs,
+  refine set_integral_congr_ae (ℱ.le i s hs) _,
+  filter_upwards [hf.2 i j hij],
+  intros _ heq _,
+  exact heq.symm,
+end
+
 lemma add (hf : martingale f ℱ μ) (hg : martingale g ℱ μ) : martingale (f + g) ℱ μ :=
 begin
   refine ⟨hf.adapted.add hg.adapted, λ i j hij, _⟩,
@@ -83,11 +117,194 @@ begin
   rw [pi.smul_apply, hx, pi.smul_apply, pi.smul_apply],
 end
 
+lemma supermartingale [preorder E] (hf : martingale f ℱ μ) : supermartingale f ℱ μ :=
+⟨hf.1, λ i j hij, (hf.2 i j hij).le, λ i, hf.integrable i⟩
+
+lemma submartingale [preorder E] (hf : martingale f ℱ μ) : submartingale f ℱ μ :=
+⟨hf.1, λ i j hij, (hf.2 i j hij).symm.le, λ i, hf.integrable i⟩
+
 end martingale
 
+lemma martingale_iff [partial_order E] : martingale f ℱ μ ↔
+  supermartingale f ℱ μ ∧ submartingale f ℱ μ :=
+⟨λ hf, ⟨hf.supermartingale, hf.submartingale⟩,
+ λ ⟨hf₁, hf₂⟩, ⟨hf₁.1, λ i j hij, (hf₁.2.1 i j hij).antisymm (hf₂.2.1 i j hij)⟩⟩
+
 lemma martingale_condexp (f : α → E) (ℱ : filtration ι m0) (μ : measure α)
   [sigma_finite_filtration μ ℱ] :
   martingale (λ i, μ[f | ℱ i, ℱ.le i]) ℱ μ :=
 ⟨λ i, measurable_condexp, λ i j hij, condexp_condexp_of_le (ℱ.mono hij) _⟩
 
+namespace supermartingale
+
+lemma adapted [has_le E] (hf : supermartingale f ℱ μ) : adapted ℱ f := hf.1
+
+lemma measurable [has_le E] (hf : supermartingale f ℱ μ) (i : ι) : measurable[ℱ i] (f i) :=
+hf.adapted i
+
+lemma integrable [has_le E] (hf : supermartingale f ℱ μ) (i : ι) : integrable (f i) μ := hf.2.2 i
+
+lemma condexp_ae_le [has_le E] (hf : supermartingale f ℱ μ) {i j : ι} (hij : i ≤ j) :
+  μ[f j | ℱ i, ℱ.le i] ≤ᵐ[μ] f i :=
+hf.2.1 i j hij
+
+lemma set_integral_le {f : ι → α → ℝ} (hf : supermartingale f ℱ μ)
+  {i j : ι} (hij : i ≤ j) {s : set α} (hs : measurable_set[ℱ i] s) :
+  ∫ x in s, f j x ∂μ ≤ ∫ x in s, f i x ∂μ :=
+begin
+  rw ← set_integral_condexp (ℱ.le i) (hf.integrable j) hs,
+  refine set_integral_mono_ae integrable_condexp.integrable_on (hf.integrable i).integrable_on _,
+  filter_upwards [hf.2.1 i j hij],
+  intros _ heq,
+  exact heq,
+end
+
+lemma add [preorder E] [covariant_class E E (+) (≤)]
+  (hf : supermartingale f ℱ μ) (hg : supermartingale g ℱ μ) : supermartingale (f + g) ℱ μ :=
+begin
+  refine ⟨hf.1.add hg.1, λ i j hij, _, λ i, (hf.2.2 i).add (hg.2.2 i)⟩,
+  refine (condexp_add (hf.integrable j) (hg.integrable j)).le.trans _,
+  filter_upwards [hf.2.1 i j hij, hg.2.1 i j hij],
+  intros,
+  refine add_le_add _ _; assumption,
+end
+
+lemma add_martingale [preorder E] [covariant_class E E (+) (≤)]
+  (hf : supermartingale f ℱ μ) (hg : martingale g ℱ μ) : supermartingale (f + g) ℱ μ :=
+hf.add hg.supermartingale
+
+lemma neg [preorder E] [covariant_class E E (+) (≤)]
+  (hf : supermartingale f ℱ μ) : submartingale (-f) ℱ μ :=
+begin
+  refine ⟨hf.1.neg, λ i j hij, _, λ i, (hf.2.2 i).neg⟩,
+  refine eventually_le.trans _ (condexp_neg (f j)).symm.le,
+  filter_upwards [hf.2.1 i j hij],
+  intros _ hle,
+  simpa,
+end
+
+end supermartingale
+
+namespace submartingale
+
+lemma adapted [has_le E] (hf : submartingale f ℱ μ) : adapted ℱ f := hf.1
+
+lemma measurable [has_le E] (hf : submartingale f ℱ μ) (i : ι) : measurable[ℱ i] (f i) :=
+hf.adapted i
+
+lemma integrable [has_le E] (hf : submartingale f ℱ μ) (i : ι) : integrable (f i) μ := hf.2.2 i
+
+lemma ae_le_condexp [has_le E] (hf : submartingale f ℱ μ) {i j : ι} (hij : i ≤ j) :
+  f i ≤ᵐ[μ] μ[f j | ℱ i, ℱ.le i] :=
+hf.2.1 i j hij
+
+lemma add [preorder E] [covariant_class E E (+) (≤)]
+  (hf : submartingale f ℱ μ) (hg : submartingale g ℱ μ) : submartingale (f + g) ℱ μ :=
+begin
+  refine ⟨hf.1.add hg.1, λ i j hij, _, λ i, (hf.2.2 i).add (hg.2.2 i)⟩,
+  refine eventually_le.trans _ (condexp_add (hf.integrable j) (hg.integrable j)).symm.le,
+  filter_upwards [hf.2.1 i j hij, hg.2.1 i j hij],
+  intros,
+  refine add_le_add _ _; assumption,
+end
+
+lemma add_martingale [preorder E] [covariant_class E E (+) (≤)]
+  (hf : submartingale f ℱ μ) (hg : martingale g ℱ μ) : submartingale (f + g) ℱ μ :=
+hf.add hg.submartingale
+
+lemma neg [preorder E] [covariant_class E E (+) (≤)]
+  (hf : submartingale f ℱ μ) : supermartingale (-f) ℱ μ :=
+begin
+  refine ⟨hf.1.neg, λ i j hij, (condexp_neg (f j)).le.trans _, λ i, (hf.2.2 i).neg⟩,
+  filter_upwards [hf.2.1 i j hij],
+  intros _ hle,
+  simpa,
+end
+
+lemma set_integral_le {f : ι → α → ℝ} (hf : submartingale f ℱ μ)
+  {i j : ι} (hij : i ≤ j) {s : set α} (hs : measurable_set[ℱ i] s) :
+  ∫ x in s, f i x ∂μ ≤ ∫ x in s, f j x ∂μ :=
+begin
+  rw [← neg_le_neg_iff, ← integral_neg, ← integral_neg],
+  exact supermartingale.set_integral_le hf.neg hij hs,
+end
+
+lemma sub_supermartingale [preorder E] [covariant_class E E (+) (≤)]
+  (hf : submartingale f ℱ μ) (hg : supermartingale g ℱ μ) : submartingale (f - g) ℱ μ :=
+by { rw sub_eq_add_neg, exact hf.add hg.neg }
+
+lemma sub_martingale [preorder E] [covariant_class E E (+) (≤)]
+  (hf : submartingale f ℱ μ) (hg : martingale g ℱ μ) : submartingale (f - g) ℱ μ :=
+hf.sub_supermartingale hg.supermartingale
+
+end submartingale
+
+namespace supermartingale
+
+lemma sub_submartingale [preorder E] [covariant_class E E (+) (≤)]
+  (hf : supermartingale f ℱ μ) (hg : submartingale g ℱ μ) : supermartingale (f - g) ℱ μ :=
+by { rw sub_eq_add_neg, exact hf.add hg.neg }
+
+lemma sub_martingale [preorder E] [covariant_class E E (+) (≤)]
+  (hf : supermartingale f ℱ μ) (hg : martingale g ℱ μ) : supermartingale (f - g) ℱ μ :=
+hf.sub_submartingale hg.submartingale
+
+section
+
+variables {F : Type*} [measurable_space F] [normed_lattice_add_comm_group F]
+  [normed_space ℝ F] [complete_space F] [borel_space F] [second_countable_topology F]
+  [ordered_smul ℝ F]
+
+lemma smul_nonneg {f : ι → α → F}
+  {c : ℝ} (hc : 0 ≤ c) (hf : supermartingale f ℱ μ) :
+  supermartingale (c • f) ℱ μ :=
+begin
+  refine ⟨hf.1.smul c, λ i j hij, _, λ i, (hf.2.2 i).smul c⟩,
+  refine (condexp_smul c (f j)).le.trans _,
+  filter_upwards [hf.2.1 i j hij],
+  intros _ hle,
+  simp,
+  exact smul_le_smul_of_nonneg hle hc,
+end
+
+lemma smul_nonpos {f : ι → α → F}
+  {c : ℝ} (hc : c ≤ 0) (hf : supermartingale f ℱ μ) :
+  submartingale (c • f) ℱ μ :=
+begin
+  rw [← neg_neg c, (by { ext i x, simp } : - -c • f = -(-c • f))],
+  exact (hf.smul_nonneg $ neg_nonneg.2 hc).neg,
+end
+
+end
+
+end supermartingale
+
+namespace submartingale
+
+section
+
+variables {F : Type*} [measurable_space F] [normed_lattice_add_comm_group F]
+  [normed_space ℝ F] [complete_space F] [borel_space F] [second_countable_topology F]
+  [ordered_smul ℝ F]
+
+lemma smul_nonneg {f : ι → α → F}
+  {c : ℝ} (hc : 0 ≤ c) (hf : submartingale f ℱ μ) :
+  submartingale (c • f) ℱ μ :=
+begin
+  rw [← neg_neg c, (by { ext i x, simp } : - -c • f = -(c • -f))],
+  exact supermartingale.neg (hf.neg.smul_nonneg hc),
+end
+
+lemma smul_nonpos {f : ι → α → F}
+  {c : ℝ} (hc : c ≤ 0) (hf : submartingale f ℱ μ) :
+  supermartingale (c • f) ℱ μ :=
+begin
+  rw [← neg_neg c, (by { ext i x, simp } : - -c • f = -(-c • f))],
+  exact (hf.smul_nonneg $ neg_nonneg.2 hc).neg,
+end
+
+end
+
+end submartingale
+
 end measure_theory