refactor: generalize unbounded_of_tendsto_atTop (#23531)

Author: fpvandoorn

Mathlib/Order/Filter/AtTopBot/Basic.lean

@@ -445,33 +445,33 @@ theorem map_div_atTop_eq_nat (k : ℕ) (hk : 0 < k) : map (fun a => a / k) atTop
     (fun a b _ => by rw [Nat.div_le_iff_le_mul_add_pred hk])
     fun b _ => by rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]; omega
 
-section IsDirected
-variable [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] {f : α → β}
+section NeBot
+variable [Preorder β] {l : Filter α} [NeBot l] {f : α → β}
 
-theorem unbounded_of_tendsto_atTop [NoMaxOrder β] (h : Tendsto f atTop atTop) :
+theorem not_bddAbove_of_tendsto_atTop [NoMaxOrder β] (h : Tendsto f l atTop) :
     ¬BddAbove (range f) := by
   rintro ⟨M, hM⟩
-  obtain ⟨a, ha⟩ := mem_atTop_sets.mp (h <| Ioi_mem_atTop M)
-  apply lt_irrefl M
-  calc
-    M < f a := ha a le_rfl
-    _ ≤ M := hM (Set.mem_range_self a)
+  have : ∀ x, f x ≤ M := by aesop
+  have : ∅ = f ⁻¹' Ioi M := by aesop (add forward safe not_le_of_lt)
+  apply Filter.empty_not_mem l
+  aesop (add safe Ioi_mem_atTop)
 
-theorem unbounded_of_tendsto_atBot [NoMinOrder β] (h : Tendsto f atTop atBot) :
-    ¬BddBelow (range f) := unbounded_of_tendsto_atTop (β := βᵒᵈ) h
+theorem not_bddBelow_of_tendsto_atBot [NoMinOrder β] (h : Tendsto f l atBot) :
+    ¬BddBelow (range f) := not_bddAbove_of_tendsto_atTop (β := βᵒᵈ) h
 
-end IsDirected
+@[deprecated (since := "2025-04-28")]
+alias unbounded_of_tendsto_atTop := not_bddAbove_of_tendsto_atTop
 
-section IsCodirected
-variable [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] [Preorder β] {f : α → β}
+@[deprecated (since := "2025-04-28")]
+alias unbounded_of_tendsto_atBot := not_bddBelow_of_tendsto_atBot
 
-theorem unbounded_of_tendsto_atTop' [NoMaxOrder β] (h : Tendsto f atBot atTop) :
-    ¬BddAbove (range f) := unbounded_of_tendsto_atTop (α := αᵒᵈ) h
+@[deprecated (since := "2025-04-28")]
+alias unbounded_of_tendsto_atTop' := not_bddAbove_of_tendsto_atTop
 
-theorem unbounded_of_tendsto_atBot' [NoMinOrder β] (h : Tendsto f atBot atBot) :
-    ¬BddBelow (range f) := unbounded_of_tendsto_atTop (α := αᵒᵈ) (β := βᵒᵈ) h
+@[deprecated (since := "2025-04-28")]
+alias unbounded_of_tendsto_atBot' := not_bddBelow_of_tendsto_atBot
 
-end IsCodirected
+end NeBot
 
 theorem HasAntitoneBasis.eventually_subset [Preorder ι] {l : Filter α} {s : ι → Set α}
     (hl : l.HasAntitoneBasis s) {t : Set α} (ht : t ∈ l) : ∀ᶠ i in atTop, s i ⊆ t :=

Mathlib/Probability/Martingale/BorelCantelli.lean

@@ -249,13 +249,13 @@ theorem Martingale.ae_not_tendsto_atTop_atTop [IsFiniteMeasure μ] (hf : Marting
     (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
     ∀ᵐ ω ∂μ, ¬Tendsto (fun n => f n ω) atTop atTop := by
   filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
-    unbounded_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)
+    not_bddAbove_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)
 
 theorem Martingale.ae_not_tendsto_atTop_atBot [IsFiniteMeasure μ] (hf : Martingale f ℱ μ)
     (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
     ∀ᵐ ω ∂μ, ¬Tendsto (fun n => f n ω) atTop atBot := by
   filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
-    unbounded_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)
+    not_bddBelow_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)
 
 namespace BorelCantelli