feat(probability/upcrossing): Doob's upcrossing estimate (#14933)

This PR proves Doob's upcrossing estimate which is central for the martingale convergence theorems.



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

docs/references.bib

@@ -1140,6 +1140,20 @@ @Article{         Joyce1982
   publisher     = {Elsevier {BV}}
 }
 
+@Book{            kallenberg2021
+  author        = {Olav Kallenberg},
+  title         = {Foundations of modern probability},
+  series        = {Probability Theory and Stochastic Modelling},
+  volume        = {99},
+  publisher     = {Springer Nature Switzerland},
+  edition       = {Third Edition},
+  year          = {2021},
+  pages         = {193},
+  isbn          = {978-3-030-61870-4; 978-3-030-61871-1},
+  doi           = {10.1007/978-3-030-61871-1},
+  url           = {https://doi.org/10.1007/978-3-030-61871-1}
+}
+
 @Book{            katz_mazur,
   author        = {Katz, Nicholas M. and Mazur, Barry},
   title         = {Arithmetic moduli of elliptic curves},

src/algebra/order/lattice_group.lean

@@ -395,6 +395,15 @@ end
 lemma pos_of_one_le (a : α) (h : 1 ≤ a) : a⁺ = a :=
 by { rw m_pos_part_def, exact sup_of_le_left h, }
 
+@[to_additive] -- pos_eq_self_of_pos_pos
+lemma pos_eq_self_of_one_lt_pos {α} [linear_order α] [comm_group α]
+  {x : α} (hx : 1 < x⁺) : x⁺ = x :=
+begin
+  rw [m_pos_part_def, right_lt_sup, not_le] at hx,
+  rw [m_pos_part_def, sup_eq_left],
+  exact hx.le
+end
+
 -- 0 ≤ a implies a⁺ = a
 @[to_additive] -- pos_of_nonpos
 lemma pos_of_le_one (a : α) (h : a ≤ 1) : a⁺ = 1 :=

src/probability/hitting_time.lean

@@ -158,6 +158,23 @@ begin
     exact hitting_le_of_mem hk₁.1 (hk₁.2.le.trans hi) hk₂, },
 end
 
+lemma hitting_eq_hitting_of_exists
+  {m₁ m₂ : ι} (h : m₁ ≤ m₂) (h' : ∃ j ∈ set.Icc n m₁, u j x ∈ s) :
+  hitting u s n m₁ x = hitting u s n m₂ x :=
+begin
+  simp only [hitting, if_pos h'],
+  obtain ⟨j, hj₁, hj₂⟩ := h',
+  rw if_pos,
+  { refine le_antisymm _ (cInf_le_cInf bdd_below_Icc.inter_of_left ⟨j, hj₁, hj₂⟩
+      (set.inter_subset_inter_left _ (set.Icc_subset_Icc_right h))),
+    refine le_cInf ⟨j, set.Icc_subset_Icc_right h hj₁, hj₂⟩ (λ i hi, _),
+    by_cases hi' : i ≤ m₁,
+    { exact cInf_le bdd_below_Icc.inter_of_left ⟨⟨hi.1.1, hi'⟩, hi.2⟩ },
+    { exact ((cInf_le bdd_below_Icc.inter_of_left ⟨hj₁, hj₂⟩).trans (hj₁.2.trans le_rfl)).trans
+        (le_of_lt (not_le.1 hi')) } },
+  exact ⟨j, ⟨hj₁.1, hj₁.2.trans h⟩, hj₂⟩,
+end
+
 end inequalities
 
 /-- A discrete hitting time is a stopping time. -/
@@ -192,6 +209,33 @@ begin
   exact this.2,
 end
 
+/-- The hitting time of a discrete process with the starting time indexed by a stopping time
+is a stopping time. -/
+lemma is_stopping_time_hitting_is_stopping_time
+  [conditionally_complete_linear_order ι] [is_well_order ι (<)] [encodable ι]
+  [topological_space ι] [order_topology ι] [first_countable_topology ι]
+  [topological_space β] [pseudo_metrizable_space β] [measurable_space β] [borel_space β]
+  {f : filtration ι m} {u : ι → α → β} {τ : α → ι} (hτ : is_stopping_time f τ)
+  {N : ι} (hτbdd : ∀ x, τ x ≤ N) {s : set β} (hs : measurable_set s) (hf : adapted f u) :
+  is_stopping_time f (λ x, hitting u s (τ x) N x) :=
+begin
+  intro n,
+  have h₁ : {x | hitting u s (τ x) N x ≤ n} =
+    (⋃ i ≤ n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) ∪
+    (⋃ i > n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}),
+  { ext x,
+    simp [← exists_or_distrib, ← or_and_distrib_right, le_or_lt] },
+  have h₂ : (⋃ i > n, {x | τ x = i} ∩ {x | hitting u s i N x ≤ n}) = ∅,
+  { ext x,
+    simp only [gt_iff_lt, set.mem_Union, set.mem_inter_eq, set.mem_set_of_eq,
+      exists_prop, set.mem_empty_eq, iff_false, not_exists, not_and, not_le],
+    rintro m hm rfl,
+    exact lt_of_lt_of_le hm (le_hitting (hτbdd _) _) },
+  rw [h₁, h₂, set.union_empty],
+  exact measurable_set.Union (λ i, measurable_set.Union_Prop
+    (λ hi, (f.mono hi _ (hτ.measurable_set_eq i)).inter (hitting_is_stopping_time hf hs n))),
+end
+
 section complete_lattice
 
 variables [complete_lattice ι] {u : ι → α → β} {s : set β} {f : filtration ι m}

src/probability/martingale.lean

@@ -62,6 +62,10 @@ filtration `ℱ` if `f` is adapted with respect to `ℱ` and for all `i ≤ j`,
 def submartingale [has_le E] (f : ι → α → E) (ℱ : filtration ι m0) (μ : measure α) : Prop :=
 adapted ℱ f ∧ (∀ i j, i ≤ j → f i ≤ᵐ[μ] μ[f j | ℱ i]) ∧ ∀ i, integrable (f i) μ
 
+lemma martingale_const (ℱ : filtration ι m0) (μ : measure α) [is_finite_measure μ] (x : E) :
+  martingale (λ _ _, x) ℱ μ :=
+⟨adapted_const ℱ _, λ i j hij, by rw condexp_const (ℱ.le _)⟩
+
 variables (E)
 lemma martingale_zero (ℱ : filtration ι m0) (μ : measure α) :
   martingale (0 : ι → α → E) ℱ μ :=

src/probability/stopping.lean

@@ -261,6 +261,9 @@ lemma strongly_measurable_le {i j : ι} (hf : adapted f u) (hij : i ≤ j) :
 
 end adapted
 
+lemma adapted_const (f : filtration ι m) (x : β) : adapted f (λ _ _, x) :=
+λ i, strongly_measurable_const
+
 variable (β)
 lemma adapted_zero [has_zero β] (f : filtration ι m) : adapted f (0 : ι → α → β) :=
 λ i, @strongly_measurable_zero α β (f i) _ _