diff --git a/Mathlib/Probability/Martingale/Upcrossing.lean b/Mathlib/Probability/Martingale/Upcrossing.lean
index 44c3143edc0e77..cb60ed523c190e 100644
--- a/Mathlib/Probability/Martingale/Upcrossing.lean
+++ b/Mathlib/Probability/Martingale/Upcrossing.lean
@@ -132,31 +132,38 @@ To obtain the general case, we simply apply the above to $((f_n - a)^+)_n$.
 
 -/
 
+section Definitions
 
+variable [Preorder ι] [OrderBot ι] [InfSet ι]
+variable {a b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {ω : Ω}
+
+omit [OrderBot ι] in
 /-- `lowerCrossingTimeAux a f c N` is the first time `f` reached below `a` after time `c` before
 time `N`. -/
-noncomputable def lowerCrossingTimeAux [Preorder ι] [InfSet ι] (a : ℝ) (f : ι → Ω → ℝ) (c N : ι) :
+noncomputable def lowerCrossingTimeAux (a : ℝ) (f : ι → Ω → ℝ) (c N : ι) :
     Ω → ι :=
   hittingBtwn f (Set.Iic a) c N
 
 /-- `upperCrossingTime a b f N n` is the first time before time `N`, `f` reaches
 above `b` after `f` reached below `a` for the `n - 1`-th time. -/
-noncomputable def upperCrossingTime [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
-    (N : ι) : ℕ → Ω → ι
+noncomputable def upperCrossingTime (a b : ℝ) (f : ι → Ω → ℝ) (N : ι) : ℕ → Ω → ι
   | 0 => ⊥
   | n + 1 => fun ω =>
     hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
 
 /-- `lowerCrossingTime a b f N n` is the first time before time `N`, `f` reaches
 below `a` after `f` reached above `b` for the `n`-th time. -/
-noncomputable def lowerCrossingTime [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
-    (N : ι) (n : ℕ) : Ω → ι :=
+noncomputable def lowerCrossingTime (a b : ℝ) (f : ι → Ω → ℝ) (N : ι) (n : ℕ) : Ω → ι :=
     fun ω => hittingBtwn f (Set.Iic a) (upperCrossingTime a b f N n ω) N ω
 
-section
+/-- The number of upcrossings (strictly) before time `N`. -/
+noncomputable def upcrossingsBefore (a b : ℝ) (f : ι → Ω → ℝ) (N : ι) (ω : Ω) : ℕ :=
+  sSup {n | upperCrossingTime a b f N n ω < N}
 
-variable [Preorder ι] [OrderBot ι] [InfSet ι]
-variable {a b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ} {ω : Ω}
+/-- The number of upcrossings of a realization of a stochastic process (`upcrossings` takes value
+in `ℝ≥0∞` and so is allowed to be `∞`). -/
+noncomputable def upcrossings (a b : ℝ) (f : ι → Ω → ℝ) (ω : Ω) : ℝ≥0∞ :=
+  ⨆ N, (upcrossingsBefore a b f N ω : ℝ≥0∞)
 
 @[simp]
 theorem upperCrossingTime_zero : upperCrossingTime a b f N 0 = ⊥ :=
@@ -176,7 +183,27 @@ theorem upperCrossingTime_succ_eq (ω : Ω) : upperCrossingTime a b f N (n + 1)
   simp only [upperCrossingTime_succ]
   rfl
 
-end
+@[simp]
+theorem upcrossingsBefore_bot : upcrossingsBefore a b f ⊥ ω = ⊥ := by simp [upcrossingsBefore]
+
+theorem upcrossings_lt_top_iff :
+    upcrossings a b f ω < ∞ ↔ ∃ k, ∀ N, upcrossingsBefore a b f N ω ≤ k := by
+  have : upcrossings a b f ω < ∞ ↔ ∃ k : ℝ≥0, upcrossings a b f ω ≤ k := by
+    constructor
+    · intro h
+      lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr
+      exact ⟨r, le_rfl⟩
+    · rintro ⟨k, hk⟩
+      exact lt_of_le_of_lt hk ENNReal.coe_lt_top
+  simp_rw [this, upcrossings, iSup_le_iff]
+  constructor <;> rintro ⟨k, hk⟩
+  · obtain ⟨m, hm⟩ := exists_nat_ge k
+    refine ⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩
+    rwa [← ENNReal.coe_natCast, ENNReal.coe_le_coe]
+  · refine ⟨k, fun N => ?_⟩
+    simp only [ENNReal.coe_natCast, Nat.cast_le, hk N]
+
+end Definitions
 
 section ConditionallyCompleteLinearOrderBot
 
@@ -216,18 +243,140 @@ theorem upperCrossingTime_mono (hnm : n ≤ m) :
   exact monotone_nat_of_le_succ fun n =>
     le_trans upperCrossingTime_le_lowerCrossingTime lowerCrossingTime_le_upperCrossingTime_succ
 
-end ConditionallyCompleteLinearOrderBot
+theorem lowerCrossingTime_stabilize (hnm : n ≤ m) (hn : lowerCrossingTime a b f N n ω = N) :
+    lowerCrossingTime a b f N m ω = N :=
+  le_antisymm lowerCrossingTime_le (le_trans (le_of_eq hn.symm) (lowerCrossingTime_mono hnm))
 
-variable {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n m : ℕ} {ω : Ω}
+theorem upperCrossingTime_stabilize (hnm : n ≤ m) (hn : upperCrossingTime a b f N n ω = N) :
+    upperCrossingTime a b f N m ω = N :=
+  le_antisymm upperCrossingTime_le (le_trans (le_of_eq hn.symm) (upperCrossingTime_mono hnm))
+
+theorem lowerCrossingTime_stabilize' (hnm : n ≤ m) (hn : N ≤ lowerCrossingTime a b f N n ω) :
+    lowerCrossingTime a b f N m ω = N :=
+  lowerCrossingTime_stabilize hnm (le_antisymm lowerCrossingTime_le hn)
+
+theorem upperCrossingTime_stabilize' (hnm : n ≤ m) (hn : N ≤ upperCrossingTime a b f N n ω) :
+    upperCrossingTime a b f N m ω = N :=
+  upperCrossingTime_stabilize hnm (le_antisymm upperCrossingTime_le hn)
+
+theorem upperCrossingTime_lt_nonempty (hN : ⊥ < N) :
+    {n | upperCrossingTime a b f N n ω < N}.Nonempty :=
+  ⟨⊥, hN⟩
+
+theorem crossing_eq_crossing_of_lowerCrossingTime_lt {M : ι} (hNM : N ≤ M)
+    (h : lowerCrossingTime a b f N n ω < N) :
+    upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
+      lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω := by
+  have h' : upperCrossingTime a b f N n ω < N :=
+    lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime h
+  induction n with
+  | zero =>
+    simp only [upperCrossingTime_zero,
+      lowerCrossingTime_zero, true_and, eq_comm]
+    refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
+    rw [lowerCrossingTime, hittingBtwn_lt_iff] at h
+    · obtain ⟨j, hj₁, hj₂⟩ := h
+      exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
+    · exact le_rfl
+  | succ k ih =>
+    specialize ih (lt_of_le_of_lt (lowerCrossingTime_mono (Nat.le_succ _)) h)
+      (lt_of_le_of_lt (upperCrossingTime_mono (Nat.le_succ _)) h')
+    have : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω := by
+      rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h'
+      · simp only [upperCrossingTime_succ_eq]
+        obtain ⟨j, hj₁, hj₂⟩ := h'
+        rw [eq_comm, ih.2]
+        exact hittingBtwn_eq_hittingBtwn_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
+      · exact le_rfl
+    refine ⟨this, ?_⟩
+    simp only [lowerCrossingTime, eq_comm, this, Nat.succ_eq_add_one]
+    refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
+    rw [lowerCrossingTime, hittingBtwn_lt_iff _ le_rfl] at h
+    obtain ⟨j, hj₁, hj₂⟩ := h
+    exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
+
+theorem crossing_eq_crossing_of_upperCrossingTime_lt {M : ι} (hNM : N ≤ M)
+    (h : upperCrossingTime a b f N (n + 1) ω < N) :
+    upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
+      lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω := by
+  have := (crossing_eq_crossing_of_lowerCrossingTime_lt hNM
+    (lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ h)).2
+  refine ⟨?_, this⟩
+  rw [upperCrossingTime_succ_eq, upperCrossingTime_succ_eq, eq_comm, this]
+  refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
+  rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h
+  · obtain ⟨j, hj₁, hj₂⟩ := h
+    exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
+  · exact le_rfl
+
+theorem upperCrossingTime_eq_upperCrossingTime_of_lt {M : ι} (hNM : N ≤ M)
+    (h : upperCrossingTime a b f N n ω < N) :
+    upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω := by
+  cases n
+  · simp
+  · exact (crossing_eq_crossing_of_upperCrossingTime_lt hNM h).1
+
+theorem crossing_pos_eq (hab : a < b) :
+    upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
+      lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n := by
+  have hab' : 0 < b - a := sub_pos.2 hab
+  have hf : ∀ ω i, b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω := by
+    intro i ω
+    refine ⟨fun h => ?_, fun h => ?_⟩
+    · rwa [← sub_le_sub_iff_right a, ←
+        posPart_eq_of_posPart_pos (lt_of_lt_of_le hab' h)]
+    · rw [← sub_le_sub_iff_right a] at h
+      rwa [posPart_eq_self.2 (le_trans hab'.le h)]
+  have hf' (ω i) : (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a := by rw [posPart_nonpos, sub_nonpos]
+  induction n with
+  | zero =>
+    refine ⟨rfl, ?_⟩
+    ext ω
+    simp only [lowerCrossingTime_zero]
+    unfold hittingBtwn
+    simp only [Set.Icc_bot, Set.mem_Iic]
+    congr! 1
+    · simp [hf']
+    · grind
+  | succ k ih =>
+    have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) =
+        upperCrossingTime a b f N (k + 1) := by
+      ext ω
+      simp only [upperCrossingTime_succ_eq, ← ih.2, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]
+      split_ifs with h₁ h₂ h₂
+      · simp_rw [← sub_le_iff_le_add, hf ω]
+      · refine False.elim (h₂ ?_)
+        simp_all only [Set.mem_Ici, not_true_eq_false]
+      · refine False.elim (h₁ ?_)
+        simp_all only [Set.mem_Ici]
+      · rfl
+    refine ⟨this, ?_⟩
+    ext ω
+    simp only [lowerCrossingTime, this, hittingBtwn, Set.mem_Iic]
+    split_ifs with h₁ h₂ h₂
+    · simp_rw [hf' ω]
+    · refine False.elim (h₂ ?_)
+      simp_all only [Set.mem_Iic, not_true_eq_false]
+    · refine False.elim (h₁ ?_)
+      simp_all only [Set.mem_Iic]
+    · rfl
+
+theorem upcrossingsBefore_pos_eq (hab : a < b) :
+    upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = upcrossingsBefore a b f N ω := by
+  simp_rw [upcrossingsBefore, (crossing_pos_eq hab).1]
+
+section WellFoundedLT
+
+variable [WellFoundedLT ι]
 
 theorem stoppedValue_lowerCrossingTime (h : lowerCrossingTime a b f N n ω ≠ N) :
-    stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N n ω : ℕ)) ω ≤ a := by
+    stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N n ω : ι)) ω ≤ a := by
   obtain ⟨j, hj₁, hj₂⟩ :=
     (hittingBtwn_le_iff_of_lt _ (lt_of_le_of_ne lowerCrossingTime_le h)).1 le_rfl
   exact stoppedValue_hittingBtwn_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 lowerCrossingTime_le⟩, hj₂⟩
 
 theorem stoppedValue_upperCrossingTime (h : upperCrossingTime a b f N (n + 1) ω ≠ N) :
-    b ≤ stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (n + 1) ω : ℕ)) ω := by
+    b ≤ stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (n + 1) ω : ι)) ω := by
   obtain ⟨j, hj₁, hj₂⟩ :=
     (hittingBtwn_le_iff_of_lt _ (lt_of_le_of_ne upperCrossingTime_le h)).1 le_rfl
   exact stoppedValue_hittingBtwn_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 (hittingBtwn_le _)⟩, hj₂⟩
@@ -255,33 +404,76 @@ theorem upperCrossingTime_lt_succ (hab : a < b) (hn : upperCrossingTime a b f N
   lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime
     (lowerCrossingTime_lt_upperCrossingTime hab hn)
 
-theorem lowerCrossingTime_stabilize (hnm : n ≤ m) (hn : lowerCrossingTime a b f N n ω = N) :
-    lowerCrossingTime a b f N m ω = N :=
-  le_antisymm lowerCrossingTime_le (le_trans (le_of_eq hn.symm) (lowerCrossingTime_mono hnm))
+variable {ℱ : Filtration ι m0}
 
-theorem upperCrossingTime_stabilize (hnm : n ≤ m) (hn : upperCrossingTime a b f N n ω = N) :
-    upperCrossingTime a b f N m ω = N :=
-  le_antisymm upperCrossingTime_le (le_trans (le_of_eq hn.symm) (upperCrossingTime_mono hnm))
+theorem StronglyAdapted.isStoppingTime_crossing [Countable ι] (hf : StronglyAdapted ℱ f) :
+    IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N n ω : ι)) ∧
+      IsStoppingTime ℱ (fun ω ↦ (lowerCrossingTime a b f N n ω : ι)) := by
+  let : TopologicalSpace ι := Preorder.topology ι
+  have : OrderTopology ι := ⟨rfl⟩
+  induction n with
+  | zero =>
+    refine ⟨isStoppingTime_const _ ⊥, ?_⟩
+    simp only [lowerCrossingTime_zero]
+    exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic
+  | succ k ih =>
+    have : IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ι)) := by
+      intro n
+      simp_rw [upperCrossingTime_succ_eq]
+      refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
+      simp [lowerCrossingTime_le]
+    refine ⟨this, fun n ↦ ?_⟩
+    refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _
+    simp [upperCrossingTime_le]
 
-theorem lowerCrossingTime_stabilize' (hnm : n ≤ m) (hn : N ≤ lowerCrossingTime a b f N n ω) :
-    lowerCrossingTime a b f N m ω = N :=
-  lowerCrossingTime_stabilize hnm (le_antisymm lowerCrossingTime_le hn)
+theorem StronglyAdapted.isStoppingTime_upperCrossingTime [Countable ι] (hf : StronglyAdapted ℱ f) :
+    IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N n ω : ι)) :=
+  hf.isStoppingTime_crossing.1
 
-theorem upperCrossingTime_stabilize' (hnm : n ≤ m) (hn : N ≤ upperCrossingTime a b f N n ω) :
-    upperCrossingTime a b f N m ω = N :=
-  upperCrossingTime_stabilize hnm (le_antisymm upperCrossingTime_le hn)
+theorem StronglyAdapted.isStoppingTime_lowerCrossingTime [Countable ι] (hf : StronglyAdapted ℱ f) :
+    IsStoppingTime ℱ (fun ω ↦ (lowerCrossingTime a b f N n ω : ι)) :=
+  hf.isStoppingTime_crossing.2
+
+end WellFoundedLT
+
+section LocallyFiniteOrder
+
+variable [LocallyFiniteOrder ι]
+
+-- TODO: move
+lemma wellFoundedLT_of_Iic {ι : Type*} [Preorder ι] (h : ∀ x : ι, WellFoundedLT (Set.Iic x)) :
+    WellFoundedLT ι := by
+  refine ⟨⟨fun x ↦ ?_⟩⟩
+  have h := (h x).wf.apply ⟨x, le_rfl⟩
+  rw [acc_iff_isEmpty_descending_chain] at h ⊢
+  contrapose! h
+  obtain ⟨f, hf⟩ := h
+  refine ⟨fun n ↦ ⟨f n, ?_⟩, by simpa using hf.1, by simpa using hf.2⟩
+  induction n with
+  | zero => simp [hf.1]
+  | succ n ih => grind
+
+-- TODO: move
+instance {ι : Type*} [Preorder ι] [LocallyFiniteOrder ι] [OrderBot ι] : WellFoundedLT ι :=
+  wellFoundedLT_of_Iic fun _ ↦ Finite.to_wellFoundedLT
 
 -- `upperCrossingTime_bound_eq` provides an explicit bound
-theorem exists_upperCrossingTime_eq (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω) (hab : a < b) :
+theorem exists_upperCrossingTime_eq
+    {ι : Type*} [ConditionallyCompleteLinearOrderBot ι] [LocallyFiniteOrder ι]
+    (f : ι → Ω → ℝ) (N : ι) (ω : Ω) (hab : a < b) :
     ∃ n, upperCrossingTime a b f N n ω = N := by
   by_contra! h
-  have : StrictMono fun n => upperCrossingTime a b f N n ω :=
+  have h_strict : StrictMono fun n => upperCrossingTime a b f N n ω :=
     strictMono_nat_of_lt_succ fun n => upperCrossingTime_lt_succ hab (h _)
-  obtain ⟨_, ⟨k, rfl⟩, hk⟩ :
-      ∃ (m : _) (_ : m ∈ Set.range fun n => upperCrossingTime a b f N n ω), N < m :=
-    ⟨upperCrossingTime a b f N (N + 1) ω, ⟨N + 1, rfl⟩,
-      lt_of_lt_of_le N.lt_succ_self (StrictMono.id_le this (N + 1))⟩
-  exact not_le.2 hk upperCrossingTime_le
+  have h_infi : Set.Infinite (Set.range fun n => upperCrossingTime a b f N n ω) :=
+    Set.infinite_range_of_injective h_strict.injective
+  have h_fin : Set.Finite (Set.range fun n => upperCrossingTime a b f N n ω) := by
+    refine Set.Finite.subset (Set.finite_Iic N) ?_
+    intro i hi
+    simp only [Set.mem_range, Set.mem_Iic] at hi ⊢
+    obtain ⟨n, rfl⟩ := hi
+    exact upperCrossingTime_le
+  exact h_infi h_fin
 
 theorem upperCrossingTime_lt_bddAbove (hab : a < b) :
     BddAbove {n | upperCrossingTime a b f N n ω < N} := by
@@ -290,9 +482,55 @@ theorem upperCrossingTime_lt_bddAbove (hab : a < b) :
   by_contra hn'
   exact hn.ne (upperCrossingTime_stabilize (not_le.1 hn').le hk)
 
-theorem upperCrossingTime_lt_nonempty (hN : 0 < N) :
-    {n | upperCrossingTime a b f N n ω < N}.Nonempty :=
-  ⟨0, hN⟩
+theorem upperCrossingTime_lt_of_le_upcrossingsBefore (hN : ⊥ < N) (hab : a < b)
+    (hn : n ≤ upcrossingsBefore a b f N ω) : upperCrossingTime a b f N n ω < N :=
+  haveI : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N :=
+    (upperCrossingTime_lt_nonempty hN).csSup_mem
+      ((OrderBot.bddBelow _).finite_of_bddAbove (upperCrossingTime_lt_bddAbove hab))
+  lt_of_le_of_lt (upperCrossingTime_mono hn) this
+
+theorem upperCrossingTime_eq_of_upcrossingsBefore_lt (hab : a < b)
+    (hn : upcrossingsBefore a b f N ω < n) : upperCrossingTime a b f N n ω = N := by
+  refine le_antisymm upperCrossingTime_le (not_lt.1 ?_)
+  convert notMem_of_csSup_lt hn (upperCrossingTime_lt_bddAbove hab) using 1
+
+theorem lowerCrossingTime_lt_of_lt_upcrossingsBefore (hN : ⊥ < N) (hab : a < b)
+    (hn : n < upcrossingsBefore a b f N ω) : lowerCrossingTime a b f N n ω < N :=
+  lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ
+    (upperCrossingTime_lt_of_le_upcrossingsBefore hN hab hn)
+
+theorem upcrossingsBefore_mono (hab : a < b) : Monotone fun N ω => upcrossingsBefore a b f N ω := by
+  intro N M hNM ω
+  simp only [upcrossingsBefore]
+  gcongr sSup {n | ?_} with n
+  · exact upperCrossingTime_lt_bddAbove hab
+  intro hn
+  rw [upperCrossingTime_eq_upperCrossingTime_of_lt hNM hn]
+  exact lt_of_lt_of_le hn hNM
+
+theorem le_sub_of_le_upcrossingsBefore (hN : ⊥ < N) (hab : a < b)
+    (hn : n < upcrossingsBefore a b f N ω) :
+    b - a ≤ stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (n + 1) ω : ι)) ω -
+      stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N n ω : ι)) ω :=
+  sub_le_sub
+    (stoppedValue_upperCrossingTime (upperCrossingTime_lt_of_le_upcrossingsBefore hN hab hn).ne)
+    (stoppedValue_lowerCrossingTime (lowerCrossingTime_lt_of_lt_upcrossingsBefore hN hab hn).ne)
+
+theorem sub_eq_zero_of_upcrossingsBefore_lt (hab : a < b) (hn : upcrossingsBefore a b f N ω < n) :
+    stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (n + 1) ω : ι)) ω -
+      stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N n ω : ι)) ω = 0 := by
+  have : N ≤ upperCrossingTime a b f N n ω := by
+    rw [upcrossingsBefore] at hn
+    rw [← not_lt]
+    exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)
+  simp [stoppedValue, upperCrossingTime_stabilize' (Nat.le_succ n) this,
+    lowerCrossingTime_stabilize' le_rfl (le_trans this upperCrossingTime_le_lowerCrossingTime)]
+
+end LocallyFiniteOrder
+
+end ConditionallyCompleteLinearOrderBot
+
+variable {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {n m : ℕ} {ω : Ω}
 
 theorem upperCrossingTime_bound_eq (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω) (hab : a < b) :
     upperCrossingTime a b f N N ω = N := by
@@ -314,32 +552,6 @@ theorem upperCrossingTime_eq_of_bound_le (hab : a < b) (hn : N ≤ n) :
 
 variable {ℱ : Filtration ℕ m0}
 
-theorem StronglyAdapted.isStoppingTime_crossing (hf : StronglyAdapted ℱ f) :
-    IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N n ω : ℕ)) ∧
-      IsStoppingTime ℱ (fun ω ↦ (lowerCrossingTime a b f N n ω : ℕ)) := by
-  induction n with
-  | zero =>
-    refine ⟨isStoppingTime_const _ 0, ?_⟩
-    simp only [lowerCrossingTime_zero, Nat.bot_eq_zero]
-    exact hf.adapted.isStoppingTime_hittingBtwn measurableSet_Iic
-  | succ k ih =>
-    have : IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) := by
-      intro n
-      simp_rw [upperCrossingTime_succ_eq]
-      refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime ih.2 ?_ measurableSet_Ici _
-      simp [lowerCrossingTime_le]
-    refine ⟨this, fun n ↦ ?_⟩
-    refine hf.adapted.isStoppingTime_hittingBtwn_isStoppingTime this ?_ measurableSet_Iic _
-    simp [upperCrossingTime_le]
-
-theorem StronglyAdapted.isStoppingTime_upperCrossingTime (hf : StronglyAdapted ℱ f) :
-    IsStoppingTime ℱ (fun ω ↦ (upperCrossingTime a b f N n ω : ℕ)) :=
-  hf.isStoppingTime_crossing.1
-
-theorem StronglyAdapted.isStoppingTime_lowerCrossingTime (hf : StronglyAdapted ℱ f) :
-    IsStoppingTime ℱ (fun ω ↦ (lowerCrossingTime a b f N n ω : ℕ)) :=
-  hf.isStoppingTime_crossing.2
-
 /-- `upcrossingStrat a b f N n` is 1 if `n` is between a consecutive pair of lower and upper
 crossings and is 0 otherwise. `upcrossingStrat` is shifted by one index so that it is adapted
 rather than predictable. -/
@@ -420,33 +632,12 @@ theorem Submartingale.sum_mul_upcrossingStrat_le [IsFiniteMeasure μ] (hf : Subm
   refine le_trans h₁ ?_
   simp_rw [Finset.sum_range_sub, integral_sub' (hf.integrable _) (hf.integrable _), le_refl]
 
-/-- The number of upcrossings (strictly) before time `N`. -/
-noncomputable def upcrossingsBefore [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
-    (N : ι) (ω : Ω) : ℕ :=
-  sSup {n | upperCrossingTime a b f N n ω < N}
-
-@[simp]
-theorem upcrossingsBefore_bot [Preorder ι] [OrderBot ι] [InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ}
-    {ω : Ω} : upcrossingsBefore a b f ⊥ ω = ⊥ := by simp [upcrossingsBefore]
-
 theorem upcrossingsBefore_zero : upcrossingsBefore a b f 0 ω = 0 := by simp [upcrossingsBefore]
 
 @[simp]
 theorem upcrossingsBefore_zero' : upcrossingsBefore a b f 0 = 0 := by
   ext ω; exact upcrossingsBefore_zero
 
-theorem upperCrossingTime_lt_of_le_upcrossingsBefore (hN : 0 < N) (hab : a < b)
-    (hn : n ≤ upcrossingsBefore a b f N ω) : upperCrossingTime a b f N n ω < N :=
-  haveI : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N :=
-    (upperCrossingTime_lt_nonempty hN).csSup_mem
-      ((OrderBot.bddBelow _).finite_of_bddAbove (upperCrossingTime_lt_bddAbove hab))
-  lt_of_le_of_lt (upperCrossingTime_mono hn) this
-
-theorem upperCrossingTime_eq_of_upcrossingsBefore_lt (hab : a < b)
-    (hn : upcrossingsBefore a b f N ω < n) : upperCrossingTime a b f N n ω = N := by
-  refine le_antisymm upperCrossingTime_le (not_lt.1 ?_)
-  convert notMem_of_csSup_lt hn (upperCrossingTime_lt_bddAbove hab) using 1
-
 theorem upcrossingsBefore_le (f : ℕ → Ω → ℝ) (ω : Ω) (hab : a < b) :
     upcrossingsBefore a b f N ω ≤ N := by
   by_cases hN : N = 0
@@ -456,68 +647,6 @@ theorem upcrossingsBefore_le (f : ℕ → Ω → ℝ) (ω : Ω) (hab : a < b) :
     by_contra hnN
     exact hn.ne (upperCrossingTime_eq_of_bound_le hab (not_le.1 hnN).le)
 
-theorem crossing_eq_crossing_of_lowerCrossingTime_lt {M : ℕ} (hNM : N ≤ M)
-    (h : lowerCrossingTime a b f N n ω < N) :
-    upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
-      lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω := by
-  have h' : upperCrossingTime a b f N n ω < N :=
-    lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime h
-  induction n with
-  | zero =>
-    simp only [upperCrossingTime_zero, bot_eq_zero',
-      lowerCrossingTime_zero, true_and, eq_comm]
-    refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
-    rw [lowerCrossingTime, hittingBtwn_lt_iff] at h
-    · obtain ⟨j, hj₁, hj₂⟩ := h
-      exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
-    · exact le_rfl
-  | succ k ih =>
-    specialize ih (lt_of_le_of_lt (lowerCrossingTime_mono (Nat.le_succ _)) h)
-      (lt_of_le_of_lt (upperCrossingTime_mono (Nat.le_succ _)) h')
-    have : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω := by
-      rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h'
-      · simp only [upperCrossingTime_succ_eq]
-        obtain ⟨j, hj₁, hj₂⟩ := h'
-        rw [eq_comm, ih.2]
-        exact hittingBtwn_eq_hittingBtwn_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
-      · exact le_rfl
-    refine ⟨this, ?_⟩
-    simp only [lowerCrossingTime, eq_comm, this, Nat.succ_eq_add_one]
-    refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
-    rw [lowerCrossingTime, hittingBtwn_lt_iff _ le_rfl] at h
-    obtain ⟨j, hj₁, hj₂⟩ := h
-    exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
-
-theorem crossing_eq_crossing_of_upperCrossingTime_lt {M : ℕ} (hNM : N ≤ M)
-    (h : upperCrossingTime a b f N (n + 1) ω < N) :
-    upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
-      lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω := by
-  have := (crossing_eq_crossing_of_lowerCrossingTime_lt hNM
-    (lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ h)).2
-  refine ⟨?_, this⟩
-  rw [upperCrossingTime_succ_eq, upperCrossingTime_succ_eq, eq_comm, this]
-  refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
-  rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h
-  · obtain ⟨j, hj₁, hj₂⟩ := h
-    exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
-  · exact le_rfl
-
-theorem upperCrossingTime_eq_upperCrossingTime_of_lt {M : ℕ} (hNM : N ≤ M)
-    (h : upperCrossingTime a b f N n ω < N) :
-    upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω := by
-  cases n
-  · simp
-  · exact (crossing_eq_crossing_of_upperCrossingTime_lt hNM h).1
-
-theorem upcrossingsBefore_mono (hab : a < b) : Monotone fun N ω => upcrossingsBefore a b f N ω := by
-  intro N M hNM ω
-  simp only [upcrossingsBefore]
-  gcongr sSup {n | ?_} with n
-  · exact upperCrossingTime_lt_bddAbove hab
-  intro hn
-  rw [upperCrossingTime_eq_upperCrossingTime_of_lt hNM hn]
-  exact lt_of_lt_of_le hn hNM
-
 theorem upcrossingsBefore_lt_of_exists_upcrossing (hab : a < b) {N₁ N₂ : ℕ} (hN₁ : N ≤ N₁)
     (hN₁' : f N₁ ω < a) (hN₂ : N₁ ≤ N₂) (hN₂' : b < f N₂ ω) :
     upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω := by
@@ -535,29 +664,6 @@ theorem upcrossingsBefore_lt_of_exists_upcrossing (hab : a < b) {N₁ N₂ : ℕ
   · rw [Nat.le_zero] at hN
     rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero, Pi.bot_apply, bot_eq_zero']
 
-theorem lowerCrossingTime_lt_of_lt_upcrossingsBefore (hN : 0 < N) (hab : a < b)
-    (hn : n < upcrossingsBefore a b f N ω) : lowerCrossingTime a b f N n ω < N :=
-  lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ
-    (upperCrossingTime_lt_of_le_upcrossingsBefore hN hab hn)
-
-theorem le_sub_of_le_upcrossingsBefore (hN : 0 < N) (hab : a < b)
-    (hn : n < upcrossingsBefore a b f N ω) :
-    b - a ≤ stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (n + 1) ω : ℕ)) ω -
-      stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N n ω : ℕ)) ω :=
-  sub_le_sub
-    (stoppedValue_upperCrossingTime (upperCrossingTime_lt_of_le_upcrossingsBefore hN hab hn).ne)
-    (stoppedValue_lowerCrossingTime (lowerCrossingTime_lt_of_lt_upcrossingsBefore hN hab hn).ne)
-
-theorem sub_eq_zero_of_upcrossingsBefore_lt (hab : a < b) (hn : upcrossingsBefore a b f N ω < n) :
-    stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (n + 1) ω : ℕ)) ω -
-      stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N n ω : ℕ)) ω = 0 := by
-  have : N ≤ upperCrossingTime a b f N n ω := by
-    rw [upcrossingsBefore] at hn
-    rw [← not_lt]
-    exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)
-  simp [stoppedValue, upperCrossingTime_stabilize' (Nat.le_succ n) this,
-    lowerCrossingTime_stabilize' le_rfl (le_trans this upperCrossingTime_le_lowerCrossingTime)]
-
 theorem mul_upcrossingsBefore_le (hf : a ≤ f N ω) (hab : a < b) :
     (b - a) * upcrossingsBefore a b f N ω ≤
     ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω := by
@@ -608,7 +714,9 @@ theorem mul_upcrossingsBefore_le (hf : a ≤ f N ω) (hab : a < b) :
           · rw [heq, sub_self]
           · rw [sub_nonneg]
             exact le_trans (stoppedValue_lowerCrossingTime heq) hf
-        · rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
+        · have h_sub := sub_eq_zero_of_upcrossingsBefore_lt hab (f := f) (ω := ω) (n := i) (N := N)
+          simp only [ENat.some_eq_coe] at h_sub
+          rw [h_sub]
           rw [Finset.mem_range, not_lt] at hi
           exact lt_of_le_of_ne hi (Ne.symm hi')
   refine le_trans ?_ h₂
@@ -628,51 +736,6 @@ theorem integral_mul_upcrossingsBefore_le_integral [IsFiniteMeasure μ] (hf : Su
     _ ≤ μ[f N] - μ[f 0] := hf.sum_mul_upcrossingStrat_le
     _ ≤ μ[f N] := (sub_le_self_iff _).2 (integral_nonneg hfzero)
 
-theorem crossing_pos_eq (hab : a < b) :
-    upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
-      lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n := by
-  have hab' : 0 < b - a := sub_pos.2 hab
-  have hf : ∀ ω i, b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω := by
-    intro i ω
-    refine ⟨fun h => ?_, fun h => ?_⟩
-    · rwa [← sub_le_sub_iff_right a, ←
-        posPart_eq_of_posPart_pos (lt_of_lt_of_le hab' h)]
-    · rw [← sub_le_sub_iff_right a] at h
-      rwa [posPart_eq_self.2 (le_trans hab'.le h)]
-  have hf' (ω i) : (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a := by rw [posPart_nonpos, sub_nonpos]
-  induction n with
-  | zero =>
-    refine ⟨rfl, ?_⟩
-    simp +unfoldPartialApp only [lowerCrossingTime_zero, hittingBtwn,
-      Set.mem_Icc, Set.mem_Iic]
-    simp_all
-  | succ k ih =>
-    have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) =
-        upperCrossingTime a b f N (k + 1) := by
-      ext ω
-      simp only [upperCrossingTime_succ_eq, ← ih.2, hittingBtwn, Set.mem_Ici, tsub_le_iff_right]
-      split_ifs with h₁ h₂ h₂
-      · simp_rw [← sub_le_iff_le_add, hf ω]
-      · refine False.elim (h₂ ?_)
-        simp_all only [Set.mem_Ici, not_true_eq_false]
-      · refine False.elim (h₁ ?_)
-        simp_all only [Set.mem_Ici]
-      · rfl
-    refine ⟨this, ?_⟩
-    ext ω
-    simp only [lowerCrossingTime, this, hittingBtwn, Set.mem_Iic]
-    split_ifs with h₁ h₂ h₂
-    · simp_rw [hf' ω]
-    · refine False.elim (h₂ ?_)
-      simp_all only [Set.mem_Iic, not_true_eq_false]
-    · refine False.elim (h₁ ?_)
-      simp_all only [Set.mem_Iic]
-    · rfl
-
-theorem upcrossingsBefore_pos_eq (hab : a < b) :
-    upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = upcrossingsBefore a b f N ω := by
-  simp_rw [upcrossingsBefore, (crossing_pos_eq hab).1]
-
 theorem mul_integral_upcrossingsBefore_le_integral_pos_part_aux [IsFiniteMeasure μ]
     (hf : Submartingale f ℱ μ) (hab : a < b) :
     (b - a) * μ[upcrossingsBefore a b f N] ≤ μ[fun ω => (f N ω - a)⁺] := by
@@ -769,33 +832,10 @@ theorem StronglyAdapted.integrable_upcrossingsBefore [IsFiniteMeasure μ]
   ⟨Measurable.aestronglyMeasurable (measurable_from_top.comp (hf.measurable_upcrossingsBefore hab)),
     .of_bounded this⟩
 
-/-- The number of upcrossings of a realization of a stochastic process (`upcrossings` takes value
-in `ℝ≥0∞` and so is allowed to be `∞`). -/
-noncomputable def upcrossings [Preorder ι] [OrderBot ι] [InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
-    (ω : Ω) : ℝ≥0∞ :=
-  ⨆ N, (upcrossingsBefore a b f N ω : ℝ≥0∞)
-
 theorem StronglyAdapted.measurable_upcrossings (hf : StronglyAdapted ℱ f) (hab : a < b) :
     Measurable (upcrossings a b f) :=
   .iSup fun _ => measurable_from_top.comp (hf.measurable_upcrossingsBefore hab)
 
-theorem upcrossings_lt_top_iff :
-    upcrossings a b f ω < ∞ ↔ ∃ k, ∀ N, upcrossingsBefore a b f N ω ≤ k := by
-  have : upcrossings a b f ω < ∞ ↔ ∃ k : ℝ≥0, upcrossings a b f ω ≤ k := by
-    constructor
-    · intro h
-      lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr
-      exact ⟨r, le_rfl⟩
-    · rintro ⟨k, hk⟩
-      exact lt_of_le_of_lt hk ENNReal.coe_lt_top
-  simp_rw [this, upcrossings, iSup_le_iff]
-  constructor <;> rintro ⟨k, hk⟩
-  · obtain ⟨m, hm⟩ := exists_nat_ge k
-    refine ⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩
-    rwa [← ENNReal.coe_natCast, ENNReal.coe_le_coe]
-  · refine ⟨k, fun N => ?_⟩
-    simp only [ENNReal.coe_natCast, Nat.cast_le, hk N]
-
 /-- A variant of Doob's upcrossing estimate obtained by taking the supremum on both sides. -/
 theorem Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part [IsFiniteMeasure μ] (a b : ℝ)
     (hf : Submartingale f ℱ μ) : ENNReal.ofReal (b - a) * ∫⁻ ω, upcrossings a b f ω ∂μ ≤