feat(probability/martingale/centering): uniqueness of Doob's decompos…

…ition (#16532)

src/probability/martingale/basic.lean

@@ -490,6 +490,41 @@ begin
   simpa only [pi.zero_apply, pi.neg_apply, zero_eq_neg],
 end
 
+-- Note that one cannot use `submartingale.zero_le_of_predictable` to prove the other two
+-- corresponding lemmas without imposing more restrictions to the ordering of `E`
+/-- A predictable submartingale is a.e. greater equal than its initial state. -/
+lemma submartingale.zero_le_of_predictable [preorder E] [sigma_finite_filtration μ 𝒢]
+  {f : ℕ → Ω → E} (hfmgle : submartingale f 𝒢 μ) (hfadp : adapted 𝒢 (λ n, f (n + 1))) (n : ℕ) :
+  f 0 ≤ᵐ[μ] f n :=
+begin
+  induction n with k ih,
+  { refl },
+  { exact ih.trans ((hfmgle.2.1 k (k + 1) k.le_succ).trans_eq $ germ.coe_eq.mp $ congr_arg coe $
+      condexp_of_strongly_measurable (𝒢.le _) (hfadp _) $ hfmgle.integrable _) }
+end
+
+/-- A predictable supermartingale is a.e. less equal than its initial state. -/
+lemma supermartingale.le_zero_of_predictable [preorder E] [sigma_finite_filtration μ 𝒢]
+  {f : ℕ → Ω → E} (hfmgle : supermartingale f 𝒢 μ) (hfadp : adapted 𝒢 (λ n, f (n + 1))) (n : ℕ) :
+  f n ≤ᵐ[μ] f 0 :=
+begin
+  induction n with k ih,
+  { refl },
+  { exact ((germ.coe_eq.mp $ congr_arg coe $ condexp_of_strongly_measurable (𝒢.le _) (hfadp _) $
+      hfmgle.integrable _).symm.trans_le (hfmgle.2.1 k (k + 1) k.le_succ)).trans ih }
+end
+
+/-- A predictable martingale is a.e. equal to its initial state. -/
+lemma martingale.eq_zero_of_predicatable [sigma_finite_filtration μ 𝒢]
+  {f : ℕ → Ω → E} (hfmgle : martingale f 𝒢 μ) (hfadp : adapted 𝒢 (λ n, f (n + 1))) (n : ℕ) :
+  f n =ᵐ[μ] f 0 :=
+begin
+  induction n with k ih,
+  { refl },
+  { exact ((germ.coe_eq.mp (congr_arg coe $ condexp_of_strongly_measurable (𝒢.le _) (hfadp _)
+      (hfmgle.integrable _))).symm.trans (hfmgle.2 k (k + 1) k.le_succ)).trans ih }
+end
+
 namespace submartingale
 
 @[protected]

src/probability/martingale/centering.lean

@@ -136,6 +136,41 @@ begin
   refl,
 end
 
+-- The following two lemmas demonstrate the essential uniqueness of the decomposition
+lemma martingale_part_add_ae_eq [sigma_finite_filtration μ ℱ] {f g : ℕ → Ω → E}
+  (hf : martingale f ℱ μ) (hg : adapted ℱ (λ n, g (n + 1))) (hg0 : g 0 = 0)
+  (hgint : ∀ n, integrable (g n) μ) (n : ℕ) :
+  martingale_part ℱ μ (f + g) n =ᵐ[μ] f n :=
+begin
+  set h := f - martingale_part ℱ μ (f + g) with hhdef,
+  have hh : h = predictable_part ℱ μ (f + g) - g,
+  { rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictable_part ℱ μ (f + g)),
+      martingale_part_add_predictable_part] },
+  have hhpred : adapted ℱ (λ n, h (n + 1)),
+  { rw hh,
+    exact adapted_predictable_part.sub hg },
+  have hhmgle : martingale h ℱ μ := hf.sub (martingale_martingale_part
+    (hf.adapted.add $ predictable.adapted hg $ hg0.symm ▸ strongly_measurable_zero) $
+    λ n, (hf.integrable n).add $ hgint n),
+  refine (eventually_eq_iff_sub.2 _).symm,
+  filter_upwards [hhmgle.eq_zero_of_predicatable hhpred n] with ω hω,
+  rw [hhdef, pi.sub_apply] at hω,
+  rw [hω, pi.sub_apply, martingale_part],
+  simp [hg0],
+end
+
+lemma predictable_part_add_ae_eq [sigma_finite_filtration μ ℱ] {f g : ℕ → Ω → E}
+  (hf : martingale f ℱ μ) (hg : adapted ℱ (λ n, g (n + 1))) (hg0 : g 0 = 0)
+  (hgint : ∀ n, integrable (g n) μ) (n : ℕ) :
+  predictable_part ℱ μ (f + g) n =ᵐ[μ] g n :=
+begin
+  filter_upwards [martingale_part_add_ae_eq hf hg hg0 hgint n] with ω hω,
+  rw ← add_right_inj (f n ω),
+  conv_rhs { rw [← pi.add_apply, ← pi.add_apply,
+    ← martingale_part_add_predictable_part ℱ μ (f + g)] },
+  rw [pi.add_apply, pi.add_apply, hω],
+end
+
 section difference
 
 lemma predictable_part_bdd_difference {R : ℝ≥0} {f : ℕ → Ω → ℝ}

src/probability/process/adapted.lean

@@ -216,4 +216,13 @@ begin
   { exact strongly_measurable_const, },
 end
 
+-- this dot notation will make more sense once we have a more general definition for predictable
+lemma predictable.adapted {f : filtration ℕ m} {u : ℕ → Ω → β}
+  (hu : adapted f (λ n, u (n + 1))) (hu0 : strongly_measurable[f 0] (u 0)) :
+  adapted f u :=
+λ n, match n with
+  | 0 := hu0
+  | n + 1 := (hu n).mono (f.mono n.le_succ)
+end
+
 end measure_theory