chore(probability/martingale/upcrossing): remove duplicate lemma (#16125

)

src/probability/martingale/upcrossing.lean

@@ -746,7 +746,7 @@ lemma upcrossings_before_pos_eq (hab : a < b) :
   upcrossings_before 0 (b - a) (λ n ω, (f n ω - a)⁺) N ω = upcrossings_before a b f N ω :=
 by simp_rw [upcrossings_before, (crossing_pos_eq hab).1]
 
-lemma mul_integral_upcrossings_before_le_integral_pos_part_aux1 [is_finite_measure μ]
+lemma mul_integral_upcrossings_before_le_integral_pos_part_aux [is_finite_measure μ]
   (hf : submartingale f ℱ μ) (hab : a < b) :
   (b - a) * μ[upcrossings_before a b f N] ≤ μ[λ ω, (f N ω - a)⁺] :=
 begin
@@ -758,11 +758,6 @@ begin
   refl,
 end
 
-lemma mul_integral_upcrossings_before_le_integral_pos_part_aux2 [is_finite_measure μ]
-  (hf : submartingale f ℱ μ) (hab : a < b) :
-  (b - a) * μ[upcrossings_before a b f N] ≤ μ[λ ω, (f N ω - a)⁺] :=
-mul_integral_upcrossings_before_le_integral_pos_part_aux1 hf hab
-
 /-- **Doob's upcrossing estimate**: given a real valued discrete submartingale `f` and real
 values `a` and `b`, we have `(b - a) * 𝔼[upcrossings_before a b f N] ≤ 𝔼[(f N - a)⁺]` where
 `upcrossings_before a b f N` is the number of times the process `f` crossed from below `a` to above
@@ -772,7 +767,7 @@ theorem submartingale.mul_integral_upcrossings_before_le_integral_pos_part [is_f
   (b - a) * μ[upcrossings_before a b f N] ≤ μ[λ ω, (f N ω - a)⁺] :=
 begin
   by_cases hab : a < b,
-  { exact mul_integral_upcrossings_before_le_integral_pos_part_aux2 hf hab },
+  { exact mul_integral_upcrossings_before_le_integral_pos_part_aux hf hab },
   { rw [not_lt, ← sub_nonpos] at hab,
     exact le_trans (mul_nonpos_of_nonpos_of_nonneg hab (integral_nonneg (λ ω, nat.cast_nonneg _)))
       (integral_nonneg (λ ω, lattice_ordered_comm_group.pos_nonneg _)) }