chore(AtTop/Monoid): add multiplicative versions (#21878)

Also review names in the file.

Moves:
- Filter.Tendsto.atTop_mul_atTop ->Filter.Tendsto.atTop_mul_atTop₀
- Filter.Tendsto.atBot_mul_atBot ->Filter.Tendsto.atBot_mul_atBot₀
- Filter.Tendsto.atTop_of_mul_const -> Filter.Tendsto.atTop_of_mul_const₀
- Filter.Tendsto.atTop_of_const_mul -> Filter.Tendsto.atTop_of_const_mul₀

Author: urkud

Mathlib/Algebra/QuadraticDiscriminant.lean

@@ -125,9 +125,9 @@ theorem discrim_le_zero (h : ∀ x : K, 0 ≤ a * (x * x) + b * x + c) : discrim
   obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0
   -- if a < 0
   · have : Tendsto (fun x => (a * x + b) * x + c) atTop atBot :=
-      tendsto_atBot_add_const_right _ c
-        ((tendsto_atBot_add_const_right _ b (tendsto_id.const_mul_atTop_of_neg ha)).atBot_mul_atTop
-          tendsto_id)
+      tendsto_atBot_add_const_right _ c <|
+        (tendsto_atBot_add_const_right _ b (tendsto_id.const_mul_atTop_of_neg ha)).atBot_mul_atTop₀
+          tendsto_id
     rcases (this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
     exact False.elim ((h x).not_lt <| by rwa [← mul_assoc, ← add_mul])
   -- if a = 0

Mathlib/Analysis/Complex/Basic.lean

@@ -150,7 +150,7 @@ theorem tendsto_abs_cocompact_atTop : Tendsto abs (cocompact ℂ) atTop :=
 /-- The `normSq` function on `ℂ` is proper. -/
 theorem tendsto_normSq_cocompact_atTop : Tendsto normSq (cocompact ℂ) atTop := by
   simpa [mul_self_abs]
-    using tendsto_abs_cocompact_atTop.atTop_mul_atTop tendsto_abs_cocompact_atTop
+    using tendsto_abs_cocompact_atTop.atTop_mul_atTop₀ tendsto_abs_cocompact_atTop
 
 open ContinuousLinearMap
 

Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

@@ -118,7 +118,7 @@ theorem tendsto_verticalIntegral (hb : 0 < b.re) (c : ℝ) :
   refine (tendsto_exp_atBot.comp (tendsto_neg_atTop_atBot.comp ?_)).const_mul _
   apply tendsto_atTop_add_const_right
   simp_rw [sq, ← mul_assoc, ← sub_mul]
-  refine Tendsto.atTop_mul_atTop (tendsto_atTop_add_const_right _ _ ?_) tendsto_id
+  refine Tendsto.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_) tendsto_id
   exact (tendsto_const_mul_atTop_of_pos hb).mpr tendsto_id
 
 theorem integrable_cexp_neg_mul_sq_add_real_mul_I (hb : 0 < b.re) (c : ℝ) :

Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

@@ -37,7 +37,7 @@ theorem exp_neg_mul_rpow_isLittleO_exp_neg {p b : ℝ} (hb : 0 < b) (hp : 1 < p)
     rw [rpow_sub_one hx.ne']
     field_simp [hx.ne']
     ring
-  apply Tendsto.atTop_mul_atTop tendsto_id
+  apply tendsto_id.atTop_mul_atTop₀
   refine tendsto_atTop_add_const_right atTop (-1 : ℝ) ?_
   exact Tendsto.const_mul_atTop hb (tendsto_rpow_atTop (by linarith))
 

Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean

@@ -40,8 +40,8 @@ lemma rexp_neg_quadratic_isLittleO_rpow_atTop {a : ℝ} (ha : a < 0) (b s : ℝ)
   have : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1)) := by
     ext1 x; ring_nf
   rw [this]
-  exact tendsto_id.atTop_mul_atTop <|
-    Filter.tendsto_atTop_add_const_right _ _ <| tendsto_id.const_mul_atTop (neg_pos.mpr ha)
+  exact tendsto_id.atTop_mul_atTop₀ <| tendsto_atTop_add_const_right _ _ <|
+    tendsto_id.const_mul_atTop (neg_pos.mpr ha)
 
 lemma cexp_neg_quadratic_isLittleO_rpow_atTop {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) :
     (fun x : ℝ ↦ cexp (a * x ^ 2 + b * x)) =o[atTop] (· ^ s) := by

Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean

@@ -248,7 +248,7 @@ theorem ruzsaSzemerediNumberNat_asymptotic_lower_bound :
         exact (isBigO_refl ..).const_mul_right (by norm_num)
       refine IsLittleO.right_isBigO_sub ?_
       simpa [div_eq_inv_mul, Function.comp_def] using
-        .atTop_of_const_mul zero_lt_three (by simp [tendsto_natCast_atTop_atTop])
+        .atTop_of_const_mul₀ zero_lt_three (by simp [tendsto_natCast_atTop_atTop])
     · rw [IsBigO_def]
       refine ⟨12, ?_⟩
       simp only [IsBigOWith, norm_natCast, eventually_atTop]

Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

@@ -112,7 +112,7 @@ lemma summable_pow_mul_jacobiTheta₂_term_bound (S : ℝ) {T : ℝ} (hT : 0 < T
   conv =>
     enter [1, n]
     rw [show -(-π * (T * n ^ 2 - 2 * S * n) - -1 * n) = n * (π * T * n - (2 * π * S + 1)) by ring]
-  refine tendsto_natCast_atTop_atTop.atTop_mul_atTop (tendsto_atTop_add_const_right _ _ ?_)
+  refine tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_)
   exact tendsto_natCast_atTop_atTop.const_mul_atTop (mul_pos pi_pos hT)
 
 /-- The series defining the theta function is summable if and only if `0 < im τ`. -/
@@ -133,7 +133,7 @@ lemma summable_jacobiTheta₂_term_iff (z τ : ℂ) : Summable (jacobiTheta₂_t
         enter [1, n]
         rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
               n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
-      refine tendsto_exp_atTop.comp (tendsto_natCast_atTop_atTop.atTop_mul_atTop ?_)
+      refine tendsto_exp_atTop.comp (tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ ?_)
       exact tendsto_atTop_add_const_right _ _ (tendsto_natCast_atTop_atTop.atTop_mul_const
         (mul_pos_of_neg_of_neg (neg_lt_zero.mpr pi_pos) hτ))
     · -- case im τ = 0: 3-way split according to `im z`

Mathlib/Order/Filter/AtTopBot/Field.lean

@@ -26,8 +26,8 @@ variable [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r c : α}
 if and only if `f` tends to infinity along the same filter. -/
 theorem tendsto_const_mul_atTop_of_pos (hr : 0 < r) :
     Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atTop :=
-  ⟨fun h => h.atTop_of_const_mul hr, fun h =>
-    Tendsto.atTop_of_const_mul (inv_pos.2 hr) <| by simpa only [inv_mul_cancel_left₀ hr.ne'] ⟩
+  ⟨fun h => h.atTop_of_const_mul₀ hr, fun h =>
+    Tendsto.atTop_of_const_mul₀ (inv_pos.2 hr) <| by simpa only [inv_mul_cancel_left₀ hr.ne'] ⟩
 
 /-- If `r` is a positive constant, `fun x ↦ f x * r` tends to infinity along a filter
 if and only if `f` tends to infinity along the same filter. -/

Mathlib/Order/Filter/AtTopBot/Group.lean

@@ -24,8 +24,7 @@ variable [OrderedAddCommGroup β] (l : Filter α) {f g : α → β}
 
 theorem tendsto_atTop_add_left_of_le' (C : β) (hf : ∀ᶠ x in l, C ≤ f x) (hg : Tendsto g l atTop) :
     Tendsto (fun x => f x + g x) l atTop :=
-  @tendsto_atTop_of_add_bdd_above_left' _ _ _ l (fun x => -f x) (fun x => f x + g x) (-C) (by simpa)
-    (by simpa)
+  .atTop_of_isBoundedUnder_le_add (f := -f) ⟨-C, by simpa⟩ (by simpa)
 
 theorem tendsto_atBot_add_left_of_ge' (C : β) (hf : ∀ᶠ x in l, f x ≤ C) (hg : Tendsto g l atBot) :
     Tendsto (fun x => f x + g x) l atBot :=
@@ -41,8 +40,7 @@ theorem tendsto_atBot_add_left_of_ge (C : β) (hf : ∀ x, f x ≤ C) (hg : Tend
 
 theorem tendsto_atTop_add_right_of_le' (C : β) (hf : Tendsto f l atTop) (hg : ∀ᶠ x in l, C ≤ g x) :
     Tendsto (fun x => f x + g x) l atTop :=
-  @tendsto_atTop_of_add_bdd_above_right' _ _ _ l (fun x => f x + g x) (fun x => -g x) (-C)
-    (by simp [hg]) (by simp [hf])
+  .atTop_of_add_isBoundedUnder_le (g := -g) ⟨-C, by simpa⟩ (by simpa)
 
 theorem tendsto_atBot_add_right_of_ge' (C : β) (hf : Tendsto f l atBot) (hg : ∀ᶠ x in l, g x ≤ C) :
     Tendsto (fun x => f x + g x) l atBot :=