feat(probability/martingale): the discrete stochastic integral of a s…

…ubmartingale is a submartingale (#14909)

This PR proves that the discrete stochastic integral of a predictable process with a submartingale is a submartingale.



Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

src/probability/martingale.lean

@@ -604,6 +604,43 @@ end
 
 end maximal
 
+lemma submartingale.sum_mul_sub [is_finite_measure μ] {R : ℝ} {ξ f : ℕ → α → ℝ}
+  (hf : submartingale f 𝒢 μ) (hξ : adapted 𝒢 ξ)
+  (hbdd : ∀ n x, ξ n x ≤ R) (hnonneg : ∀ n x, 0 ≤ ξ n x) :
+  submartingale (λ n : ℕ, ∑ k in finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ :=
+begin
+  have hξbdd : ∀ i, ∃ (C : ℝ), ∀ (x : α), |ξ i x| ≤ C :=
+    λ i, ⟨R, λ x, (abs_of_nonneg (hnonneg i x)).trans_le (hbdd i x)⟩,
+  have hint : ∀ m, integrable (∑ k in finset.range m, ξ k * (f (k + 1) - f k)) μ :=
+    λ m, integrable_finset_sum' _
+      (λ i hi, integrable.bdd_mul ((hf.integrable _).sub (hf.integrable _))
+      hξ.strongly_measurable.ae_strongly_measurable (hξbdd _)),
+  have hadp : adapted 𝒢 (λ (n : ℕ), ∑ (k : ℕ) in finset.range n, ξ k * (f (k + 1) - f k)),
+  { intro m,
+    refine finset.strongly_measurable_sum' _ (λ i hi, _),
+    rw finset.mem_range at hi,
+    exact (hξ.strongly_measurable_le hi.le).mul
+      ((hf.adapted.strongly_measurable_le (nat.succ_le_of_lt hi)).sub
+      (hf.adapted.strongly_measurable_le hi.le)) },
+  refine submartingale_of_condexp_sub_nonneg_nat hadp hint (λ i, _),
+  simp only [← finset.sum_Ico_eq_sub _ (nat.le_succ _), finset.sum_apply, pi.mul_apply,
+    pi.sub_apply, nat.Ico_succ_singleton, finset.sum_singleton],
+  exact eventually_le.trans (eventually_le.mul_nonneg (eventually_of_forall (hnonneg _))
+    (hf.condexp_sub_nonneg (nat.le_succ _))) (condexp_strongly_measurable_mul (hξ _)
+    (((hf.integrable _).sub (hf.integrable _)).bdd_mul
+      hξ.strongly_measurable.ae_strongly_measurable (hξbdd _))
+    ((hf.integrable _).sub (hf.integrable _))).symm.le,
+end
+
+/-- Given a discrete submartingale `f` and a predictable process `ξ` (i.e. `ξ (n + 1)` is adapted)
+the process defined by `λ n, ∑ k in finset.range n, ξ (k + 1) * (f (k + 1) - f k)` is also a
+submartingale. -/
+lemma submartingale.sum_mul_sub' [is_finite_measure μ] {R : ℝ} {ξ f : ℕ → α → ℝ}
+  (hf : submartingale f 𝒢 μ) (hξ : adapted 𝒢 (λ n, ξ (n + 1)))
+  (hbdd : ∀ n x, ξ n x ≤ R) (hnonneg : ∀ n x, 0 ≤ ξ n x) :
+  submartingale (λ n : ℕ, ∑ k in finset.range n, ξ (k + 1) * (f (k + 1) - f k)) 𝒢 μ :=
+hf.sum_mul_sub hξ (λ n, hbdd _) (λ n, hnonneg _)
+
 end nat
 
 end measure_theory

src/probability/stopping.lean

@@ -238,17 +238,27 @@ def adapted (f : filtration ι m) (u : ι → α → β) : Prop :=
 
 namespace adapted
 
-lemma add [has_add β] [has_continuous_add β] (hu : adapted f u) (hv : adapted f v) :
-  adapted f (u + v) :=
-λ i, (hu i).add (hv i)
+@[protected, to_additive] lemma mul [has_mul β] [has_continuous_mul β]
+  (hu : adapted f u) (hv : adapted f v) :
+  adapted f (u * v) :=
+λ i, (hu i).mul (hv i)
 
-lemma neg [add_group β] [topological_add_group β] (hu : adapted f u) : adapted f (-u) :=
-λ i, (hu i).neg
+@[protected, to_additive] lemma inv [group β] [topological_group β] (hu : adapted f u) :
+  adapted f u⁻¹ :=
+λ i, (hu i).inv
 
-lemma smul [has_smul ℝ β] [has_continuous_smul ℝ β] (c : ℝ) (hu : adapted f u) :
+@[protected] lemma smul [has_smul ℝ β] [has_continuous_smul ℝ β] (c : ℝ) (hu : adapted f u) :
   adapted f (c • u) :=
 λ i, (hu i).const_smul c
 
+@[protected] lemma strongly_measurable {i : ι} (hf : adapted f u) :
+  strongly_measurable[m] (u i) :=
+(hf i).mono (f.le i)
+
+lemma strongly_measurable_le {i j : ι} (hf : adapted f u) (hij : i ≤ j) :
+  strongly_measurable[f j] (u i) :=
+(hf i).mono (f.mono hij)
+
 end adapted
 
 variable (β)