From 61dd343281403dc60e29c793d1d2ce011debac2c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?= <Remydegenne@gmail.com>
Date: Thu, 9 Dec 2021 21:51:35 +0000
Subject: [PATCH] feat(probability_theory/martingale): define martingales
 (#10625)

Co-authored-by: RemyDegenne <remydegenne@gmail.com>
---
 .../function/conditional_expectation.lean     | 15 +++
 src/measure_theory/measure/measure_space.lean |  8 ++
 src/probability_theory/martingale.lean        | 93 +++++++++++++++++++
 3 files changed, 116 insertions(+)
 create mode 100644 src/probability_theory/martingale.lean

diff --git a/src/measure_theory/function/conditional_expectation.lean b/src/measure_theory/function/conditional_expectation.lean
index e83b19edbb390..fd2fa4714bfd6 100644
--- a/src/measure_theory/function/conditional_expectation.lean
+++ b/src/measure_theory/function/conditional_expectation.lean
@@ -1768,6 +1768,21 @@ begin
   exact (condexp_add hf hg.neg).trans (eventually_eq.rfl.add (condexp_neg g)),
 end
 
+lemma condexp_condexp_of_le {m₁ m₂ m0 : measurable_space α} {μ : measure α}
+  (hm₁₂ : m₁ ≤ m₂) (hm₂ : m₂ ≤ m0) [sigma_finite (μ.trim (hm₁₂.trans hm₂))]
+  [sigma_finite (μ.trim hm₂)] :
+  μ[ μ[f|m₂, hm₂] | m₁, hm₁₂.trans hm₂] =ᵐ[μ] μ[f | m₁, hm₁₂.trans hm₂] :=
+begin
+  refine ae_eq_of_forall_set_integral_eq_of_sigma_finite' (hm₁₂.trans hm₂)
+    (λ 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,
+  by_cases hf : integrable f μ,
+  { 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
+
 section real
 
 lemma rn_deriv_ae_eq_condexp {f : α → ℝ} (hf : integrable f μ) :
diff --git a/src/measure_theory/measure/measure_space.lean b/src/measure_theory/measure/measure_space.lean
index 4bff4e1fd3d9c..6b806a37a9d16 100644
--- a/src/measure_theory/measure/measure_space.lean
+++ b/src/measure_theory/measure/measure_space.lean
@@ -2630,6 +2630,14 @@ lemma ae_eq_of_ae_eq_trim {E} {hm : m ≤ m0} {f₁ f₂ : α → E}
   f₁ =ᵐ[μ] f₂ :=
 measure_eq_zero_of_trim_eq_zero hm h12
 
+lemma trim_trim {m₁ m₂ : measurable_space α} {hm₁₂ : m₁ ≤ m₂} {hm₂ : m₂ ≤ m0} :
+  (μ.trim hm₂).trim hm₁₂ = μ.trim (hm₁₂.trans hm₂) :=
+begin
+  ext1 t ht,
+  rw [trim_measurable_set_eq hm₁₂ ht, trim_measurable_set_eq (hm₁₂.trans hm₂) ht,
+    trim_measurable_set_eq hm₂ (hm₁₂ t ht)],
+end
+
 lemma restrict_trim (hm : m ≤ m0) (μ : measure α) (hs : @measurable_set α m s) :
   @measure.restrict α m (μ.trim hm) s = (μ.restrict s).trim hm :=
 begin
diff --git a/src/probability_theory/martingale.lean b/src/probability_theory/martingale.lean
new file mode 100644
index 0000000000000..4bb1307a1e30a
--- /dev/null
+++ b/src/probability_theory/martingale.lean
@@ -0,0 +1,93 @@
+/-
+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
+-/
+
+import probability_theory.stopping
+import measure_theory.function.conditional_expectation
+
+/-!
+# Martingales
+
+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`.
+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 `μ`.
+
+### Results
+
+* `measure_theory.martingale_condexp f ℱ μ`: the sequence `λ i, μ[f | ℱ i, ℱ.le i])` is a
+  martingale with respect to `ℱ` and `μ`.
+
+-/
+
+open topological_space filter
+open_locale nnreal ennreal measure_theory
+
+namespace measure_theory
+
+variables {α E ι : Type*} [preorder ι] [measurable_space E]
+  {m0 : measurable_space α} {μ : measure α}
+  [normed_group E] [normed_space ℝ E] [complete_space E] [borel_space E]
+  [second_countable_topology E]
+  {f g : ι → α → E} {ℱ : filtration ι m0} [sigma_finite_filtration μ ℱ]
+
+/-- A family of functions `f : ι → α → E` is a martingale with respect to a filtration `ℱ` if `f`
+is adapted with respect to `ℱ` and for all `i ≤ j`, `μ[f j | ℱ.le i] =ᵐ[μ] f i`. -/
+def martingale (f : ι → α → E) (ℱ : filtration ι m0) (μ : measure α)
+  [sigma_finite_filtration μ ℱ] : Prop :=
+adapted ℱ f ∧ ∀ i j, i ≤ j → μ[f j | ℱ i, ℱ.le i] =ᵐ[μ] f i
+
+variables (E)
+lemma martingale_zero (ℱ : filtration ι m0) (μ : measure α) [sigma_finite_filtration μ ℱ] :
+  martingale (0 : ι → α → E) ℱ μ :=
+⟨adapted_zero E ℱ, λ i j hij, by { rw [pi.zero_apply, condexp_zero], simp, }⟩
+variables {E}
+
+namespace martingale
+
+lemma adapted (hf : martingale f ℱ μ) : adapted ℱ f := hf.1
+
+lemma measurable (hf : martingale f ℱ μ) (i : ι) : measurable[ℱ i] (f i) := hf.adapted i
+
+lemma condexp_ae_eq (hf : martingale f ℱ μ) {i j : ι} (hij : i ≤ j) :
+  μ[f j | ℱ i, ℱ.le i] =ᵐ[μ] f i :=
+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 add (hf : martingale f ℱ μ) (hg : martingale g ℱ μ) : martingale (f + g) ℱ μ :=
+begin
+  refine ⟨hf.adapted.add hg.adapted, λ i j hij, _⟩,
+  exact (condexp_add (hf.integrable j) (hg.integrable j)).trans
+    ((hf.2 i j hij).add (hg.2 i j hij)),
+end
+
+lemma neg (hf : martingale f ℱ μ) : martingale (-f) ℱ μ :=
+⟨hf.adapted.neg, λ i j hij, (condexp_neg (f j)).trans ((hf.2 i j hij).neg)⟩
+
+lemma sub (hf : martingale f ℱ μ) (hg : martingale g ℱ μ) : martingale (f - g) ℱ μ :=
+by { rw sub_eq_add_neg, exact hf.add hg.neg, }
+
+lemma smul (c : ℝ) (hf : martingale f ℱ μ) : martingale (c • f) ℱ μ :=
+begin
+  refine ⟨hf.adapted.smul c, λ i j hij, _⟩,
+  refine (condexp_smul c (f j)).trans ((hf.2 i j hij).mono (λ x hx, _)),
+  rw [pi.smul_apply, hx, pi.smul_apply, pi.smul_apply],
+end
+
+end martingale
+
+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) _⟩
+
+end measure_theory