feat(probability_theory/martingale): one direction of the optional st…

…opping theorem (#11007)

src/probability_theory/martingale.lean

@@ -5,7 +5,7 @@ Authors: Rémy Degenne, Kexing Ying
 -/
 
 import probability_theory.stopping
-import measure_theory.function.conditional_expectation
+import probability_theory.notation
 
 /-!
 # Martingales
@@ -37,7 +37,7 @@ The definitions of filtration and adapted can be found in `probability_theory.st
 -/
 
 open topological_space filter
-open_locale nnreal ennreal measure_theory
+open_locale nnreal ennreal measure_theory probability_theory big_operators
 
 namespace measure_theory
 
@@ -75,14 +75,17 @@ variables {E}
 
 namespace martingale
 
+@[protected]
 lemma adapted (hf : martingale f ℱ μ) : adapted ℱ f := hf.1
 
+@[protected]
 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
 
+@[protected]
 lemma integrable (hf : martingale f ℱ μ) (i : ι) : integrable (f i) μ :=
 integrable_condexp.congr (hf.condexp_ae_eq (le_refl i))
 
@@ -137,11 +140,14 @@ lemma martingale_condexp (f : α → E) (ℱ : filtration ι m0) (μ : measure 
 
 namespace supermartingale
 
+@[protected]
 lemma adapted [has_le E] (hf : supermartingale f ℱ μ) : adapted ℱ f := hf.1
 
+@[protected]
 lemma measurable [has_le E] (hf : supermartingale f ℱ μ) (i : ι) : measurable[ℱ i] (f i) :=
 hf.adapted i
 
+@[protected]
 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) :
@@ -187,11 +193,14 @@ end supermartingale
 
 namespace submartingale
 
+@[protected]
 lemma adapted [has_le E] (hf : submartingale f ℱ μ) : adapted ℱ f := hf.1
 
+@[protected]
 lemma measurable [has_le E] (hf : submartingale f ℱ μ) (i : ι) : measurable[ℱ i] (f i) :=
 hf.adapted i
 
+@[protected]
 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) :
@@ -307,4 +316,51 @@ end
 
 end submartingale
 
+section nat
+
+variables {𝒢 : filtration ℕ m0} [sigma_finite_filtration μ 𝒢]
+
+namespace submartingale
+
+lemma integrable_stopped_value [has_le E] {f : ℕ → α → E} (hf : submartingale f 𝒢 μ) {τ : α → ℕ}
+  (hτ : is_stopping_time 𝒢 τ) {N : ℕ} (hbdd : ∀ x, τ x ≤ N) :
+  integrable (stopped_value f τ) μ :=
+integrable_stopped_value hτ hf.integrable hbdd
+
+-- We may generalize the below lemma to functions taking value in a `normed_lattice_add_comm_group`.
+-- Similarly, generalize `(super/)submartingale.set_integral_le`.
+
+/-- Given a submartingale `f` and bounded stopping times `τ` and `π` such that `τ ≤ π`, the
+expectation of `stopped_value f τ` is less or equal to the expectation of `stopped_value f π`.
+This is the forward direction of the optional stopping theorem. -/
+lemma expected_stopped_value_mono {f : ℕ → α → ℝ} (hf : submartingale f 𝒢 μ) {τ π : α → ℕ}
+  (hτ : is_stopping_time 𝒢 τ) (hπ : is_stopping_time 𝒢 π) (hle : τ ≤ π)
+  {N : ℕ} (hbdd : ∀ x, π x ≤ N) :
+  μ[stopped_value f τ] ≤ μ[stopped_value f π] :=
+begin
+  rw [← sub_nonneg, ← integral_sub', stopped_value_sub_eq_sum' hle hbdd],
+  { simp only [finset.sum_apply],
+    have : ∀ i, measurable_set[𝒢 i] {x : α | τ x ≤ i ∧ i < π x},
+    { intro i,
+      refine (hτ i).inter _,
+      convert (hπ i).compl,
+      ext x,
+      simpa },
+    rw integral_finset_sum,
+    { refine finset.sum_nonneg (λ i hi, _),
+      rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg],
+      { exact hf.set_integral_le (nat.le_succ i) (this _) },
+      { exact (hf.integrable _).integrable_on },
+      { exact (hf.integrable _).integrable_on } },
+    intros i hi,
+    exact integrable.indicator (integrable.sub (hf.integrable _) (hf.integrable _))
+      (𝒢.le _ _ (this _)) },
+  { exact hf.integrable_stopped_value hπ hbdd },
+  { exact hf.integrable_stopped_value hτ (λ x, le_trans (hle x) (hbdd x)) }
+end
+
+end submartingale
+
+end nat
+
 end measure_theory

src/probability_theory/stopping.lean

@@ -171,6 +171,20 @@ lemma is_stopping_time.measurable_set_eq_le
   measurable_set[f j] {x | τ x = i} :=
 f.mono hle _ $ hτ.measurable_set_eq i
 
+lemma is_stopping_time.measurable_set_lt (hτ : is_stopping_time f τ) (i : ℕ) :
+  measurable_set[f i] {x | τ x < i} :=
+begin
+  convert (hτ i).diff (hτ.measurable_set_eq i),
+  ext,
+  change τ x < i ↔ τ x ≤ i ∧ τ x ≠ i,
+  rw lt_iff_le_and_ne,
+end
+
+lemma is_stopping_time.measurable_set_lt_le
+  (hτ : is_stopping_time f τ) {i j : ℕ} (hle : i ≤ j) :
+  measurable_set[f j] {x | τ x < i} :=
+f.mono hle _ $ hτ.measurable_set_lt i
+
 lemma is_stopping_time_of_measurable_set_eq
   {f : filtration ℕ m} {τ : α → ℕ} (hτ : ∀ i, measurable_set[f i] {x | τ x = i}) :
   is_stopping_time f τ :=
@@ -355,12 +369,49 @@ section nat
 
 open filtration
 
-variables {f : filtration ℕ m} {u : ℕ → α → β} {τ : α → ℕ}
+variables {f : filtration ℕ m} {u : ℕ → α → β} {τ π : α → ℕ}
+
+lemma stopped_value_sub_eq_sum [add_comm_group β] (hle : τ ≤ π) :
+  stopped_value u π - stopped_value u τ =
+  λ x, (∑ i in finset.Ico (τ x) (π x), (u (i + 1) - u i)) x :=
+begin
+  ext x,
+  rw [finset.sum_Ico_eq_sub _ (hle x), finset.sum_range_sub, finset.sum_range_sub],
+  simp [stopped_value],
+end
+
+lemma stopped_value_sub_eq_sum' [add_comm_group β] (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ x, π x ≤ N) :
+  stopped_value u π - stopped_value u τ =
+  λ x, (∑ i in finset.range (N + 1),
+    set.indicator {x | τ x ≤ i ∧ i < π x} (u (i + 1) - u i)) x :=
+begin
+  rw stopped_value_sub_eq_sum hle,
+  ext x,
+  simp only [finset.sum_apply, finset.sum_indicator_eq_sum_filter],
+  refine finset.sum_congr _ (λ _ _, rfl),
+  ext i,
+  simp only [finset.mem_filter, set.mem_set_of_eq, finset.mem_range, finset.mem_Ico],
+  exact ⟨λ h, ⟨lt_trans h.2 (nat.lt_succ_iff.2 $ hbdd _), h⟩, λ h, h.2⟩
+end
 
 section add_comm_monoid
 
 variables [add_comm_monoid β]
 
+lemma stopped_value_eq {N : ℕ} (hbdd : ∀ x, τ x ≤ N) :
+  stopped_value u τ =
+  λ x, (∑ i in finset.range (N + 1), set.indicator {x | τ x = i} (u i)) x :=
+begin
+  ext y,
+  rw [stopped_value, finset.sum_apply, finset.sum_eq_single (τ y)],
+  { rw set.indicator_of_mem,
+    exact rfl },
+  { exact λ i hi hneq, set.indicator_of_not_mem hneq.symm _ },
+  { intro hy,
+    rw set.indicator_of_not_mem,
+    exact λ _, hy (finset.mem_range.2 $ lt_of_le_of_lt (hbdd _) (nat.lt_succ_self _)) }
+end
+
 lemma stopped_process_eq (n : ℕ) :
   stopped_process u τ n =
   set.indicator {a | n ≤ τ a} (u n) +
@@ -421,9 +472,9 @@ lemma mem_ℒp_stopped_process {p : ℝ≥0∞} [borel_space β] {μ : measure 
 begin
   rw stopped_process_eq,
   refine mem_ℒp.add _ _,
-  { exact mem_ℒp.indicator (f.le n {a : α | n ≤ τ a} (hτ.measurable_set_ge n)) (hu n), },
+  { exact mem_ℒp.indicator (f.le n {a : α | n ≤ τ a} (hτ.measurable_set_ge n)) (hu n) },
   { suffices : mem_ℒp (λ x, ∑ (i : ℕ) in finset.range n, {a : α | τ a = i}.indicator (u i) x) p μ,
-      by { convert this, ext1 x, simp only [finset.sum_apply], },
+    { convert this, ext1 x, simp only [finset.sum_apply] },
     refine mem_ℒp_finset_sum _ (λ i hi, mem_ℒp.indicator _ (hu i)),
     exact f.le i {a : α | τ a = i} (hτ.measurable_set_eq i) },
 end
@@ -436,6 +487,26 @@ begin
   exact mem_ℒp_stopped_process hτ hu n,
 end
 
+lemma mem_ℒp_stopped_value {p : ℝ≥0∞} [borel_space β] {μ : measure α} (hτ : is_stopping_time f τ)
+  (hu : ∀ n, mem_ℒp (u n) p μ) {N : ℕ} (hbdd : ∀ x, τ x ≤ N) :
+  mem_ℒp (stopped_value u τ) p μ :=
+begin
+  rw stopped_value_eq hbdd,
+  suffices : mem_ℒp (λ x, ∑ (i : ℕ) in finset.range (N + 1),
+    {a : α | τ a = i}.indicator (u i) x) p μ,
+  { convert this, ext1 x, simp only [finset.sum_apply] },
+  refine mem_ℒp_finset_sum _ (λ i hi, mem_ℒp.indicator _ (hu i)),
+  exact f.le i {a : α | τ a = i} (hτ.measurable_set_eq i)
+end
+
+lemma integrable_stopped_value [borel_space β] {μ : measure α} (hτ : is_stopping_time f τ)
+  (hu : ∀ n, integrable (u n) μ) {N : ℕ} (hbdd : ∀ x, τ x ≤ N) :
+  integrable (stopped_value u τ) μ :=
+begin
+  simp_rw ← mem_ℒp_one_iff_integrable at hu ⊢,
+  exact mem_ℒp_stopped_value hτ hu hbdd,
+end
+
 end normed_group
 
 end nat