chore(order/filter/at_top_bot): add/rename lemmas about limits like `…

…±∞*c` (#5333)

### New lemmas

* `filter.tendsto.nsmul_at_top` and `filter.tendsto.nsmul_at_bot`;
* `filter.tendsto_mul_self_at_top`;
* `filter.tendsto.at_top_mul_at_bot`, `filter.tendsto.at_bot_mul_at_top`,
  `filter.tendsto.at_bot_mul_at_bot`;
* `filter.tendsto.at_top_of_const_mul`, `filter.tendsto.at_top_of_mul_const`;
* `filter.tendsto.at_top_div_const`, `filter.tendsto.neg_const_mul_at_top`,
  `filter.tendsto.at_top_mul_neg_const`, `filter.tendsto.const_mul_at_bot`,
  `filter.tendsto.at_bot_mul_const`, `filer.tendsto.at_bot_div_const`,
  `filter.tendsto.neg_const_mul_at_bot`, `filter.tendsto.at_bot_mul_neg_const`.

### Renamed lemmas

* `tendsto_pow_at_top` → `filter.tendsto_pow_at_top`;
* `tendsto_at_top_mul_left` → `filter.tendsto.const_mul_at_top'`;
* `tendsto_at_top_mul_right` → `filter.tendsto.at_top_mul_const'`;
* `tendsto_at_top_mul_left'` → `filter.tendsto.const_mul_at_top`;
* `tendsto_at_top_mul_right'` → `filer.tendsto.at_top_mul_const`;
* `tendsto_mul_at_top` → `filter.tendsto.at_top_mul`;
* `tendsto_mul_at_bot` → `filter.tendsto.at_top_mul_neg`;
* `tendsto_at_top_mul_at_top` → `filter.tendsto.at_top_mul_at_top`.

src/analysis/asymptotic_equivalent.lean

@@ -251,7 +251,7 @@ variables {α β : Type*} [normed_linear_ordered_field β] {u v : α → β} {l
 lemma is_equivalent.tendsto_at_top [order_topology β] (huv : u ~[l] v) (hu : tendsto u l at_top) :
   tendsto v l at_top :=
 let ⟨φ, hφ, h⟩ := huv.symm.exists_eq_mul in
-tendsto.congr' h.symm ((mul_comm u φ) ▸ (tendsto_mul_at_top zero_lt_one hu hφ))
+tendsto.congr' h.symm ((mul_comm u φ) ▸ (hu.at_top_mul zero_lt_one hφ))
 
 lemma is_equivalent.tendsto_at_top_iff [order_topology β] (huv : u ~[l] v) :
   tendsto u l at_top ↔ tendsto v l at_top := ⟨huv.tendsto_at_top, huv.symm.tendsto_at_top⟩

src/analysis/special_functions/exp_log.lean

@@ -673,8 +673,8 @@ begin
   have B : ∀ᶠ x in at_top, exp (x / (n+1)) / (n+1)^n ≤ exp x / x^n :=
     mem_at_top_sets.2 ⟨1, λx hx, A _ (lt_of_lt_of_le zero_lt_one hx)⟩,
   have C : tendsto (λx, exp (x / (n+1)) / (n+1)^n) at_top at_top :=
-    tendsto_at_top_div (pow_pos n_pos n)
-      (tendsto_exp_at_top.comp (tendsto_at_top_div (nat.cast_add_one_pos n) tendsto_id)),
+    (tendsto_exp_at_top.comp (tendsto_id.at_top_div_const
+      (nat.cast_add_one_pos n))).at_top_div_const (pow_pos n_pos n),
   exact tendsto_at_top_mono' at_top B C
 end
 
@@ -689,7 +689,7 @@ lemma tendsto_mul_exp_add_div_pow_at_top (b c : ℝ) (n : ℕ) (hb : 0 < b) (hn
   tendsto (λ x, (b * (exp x) + c) / (x^n)) at_top at_top :=
 begin
   refine tendsto.congr' (eventually_eq_of_mem (Ioi_mem_at_top 0) _)
-    (tendsto_at_top_add_tendsto_right (tendsto_at_top_mul_left hb (tendsto_exp_div_pow_at_top n))
+    (tendsto_at_top_add_tendsto_right ( (tendsto_exp_div_pow_at_top n).const_mul_at_top hb)
       ((tendsto_pow_neg_at_top hn).mul (@tendsto_const_nhds _ _ _ c _))),
   intros x hx,
   simp only [fpow_neg x n],

src/analysis/special_functions/trigonometric.lean

@@ -2373,11 +2373,9 @@ end
 
 lemma tendsto_tan_pi_div_two : tendsto tan (𝓝[Iio (π/2)] (π/2)) at_top :=
 begin
-  convert tendsto_mul_at_top (by norm_num) (tendsto.inv_tendsto_zero tendsto_cos_pi_div_two)
+  convert (tendsto.inv_tendsto_zero tendsto_cos_pi_div_two).at_top_mul (by norm_num)
             tendsto_sin_pi_div_two,
-  ext x,
-  rw tan_eq_sin_div_cos x,
-  ring,
+  simp only [pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]
 end
 
 lemma tendsto_sin_neg_pi_div_two : tendsto sin (𝓝[Ioi (-(π/2))] (-(π/2))) (𝓝 (-1)) :=
@@ -2393,11 +2391,9 @@ end
 
 lemma tendsto_tan_neg_pi_div_two : tendsto tan (𝓝[Ioi (-(π/2))] (-(π/2))) at_bot :=
 begin
-  convert tendsto_mul_at_bot (by norm_num) (tendsto.inv_tendsto_zero tendsto_cos_neg_pi_div_two)
+  convert (tendsto.inv_tendsto_zero tendsto_cos_neg_pi_div_two).at_top_mul_neg (by norm_num)
             tendsto_sin_neg_pi_div_two,
-  ext x,
-  rw tan_eq_sin_div_cos x,
-  ring,
+  simp only [pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]
 end
 
 /-!

src/analysis/specific_limits.lean

@@ -112,17 +112,10 @@ then it goes to +∞. -/
 lemma tendsto_at_top_of_geom_lt {v : ℕ → ℝ} {k : ℝ} (h₀ : 0 < v 0) (hk : 1 < k)
   (hu : ∀ n, k*v n < v (n+1)) : tendsto v at_top at_top :=
 begin
-  apply tendsto_at_top_mono,
-  show ∀ n, k^n*v 0 ≤ v n,
-  { intro n,
-    induction n with n ih,
-    { simp },
-    calc
-    k ^ (n + 1) * v 0 = k*(k^n*v 0) : by ring_exp
-                  ... ≤ k*v n       : mul_le_mul_of_nonneg_left ih (by linarith)
-                  ... ≤ v (n + 1)   : le_of_lt (hu n) },
-  apply tendsto_at_top_mul_right h₀,
-  exact tendsto_pow_at_top_at_top_of_one_lt hk,
+  refine tendsto_at_top_mono _ ((tendsto_pow_at_top_at_top_of_one_lt hk).at_top_mul_const h₀),
+  rintro (_|n),
+  { simp },
+  { exact (geom_lt (zero_lt_one.trans hk) (λ m hm, hu m)).le }
 end
 
 lemma nnreal.tendsto_pow_at_top_nhds_0_of_lt_1 {r : nnreal} (hr : r < 1) :

src/order/filter/archimedean.lean

@@ -44,3 +44,42 @@ lemma tendsto_coe_rat_at_top_iff [linear_ordered_field R] [archimedean R]
   tendsto (λ n, (f n : R)) l at_top ↔ tendsto f l at_top :=
 tendsto_at_top_embedding (assume a₁ a₂, rat.cast_le) $
   assume r, let ⟨n, hn⟩ := exists_nat_ge r in ⟨(n:ℚ), by assumption_mod_cast⟩
+
+variables [linear_ordered_semiring R] [archimedean R]
+variables {l : filter α} {f : α → R} {r : R}
+
+/-- If a function tends to infinity along a filter, then this function multiplied by a positive
+constant (on the left) also tends to infinity. The archimedean assumption is convenient to get a
+statement that works on `ℕ`, `ℤ` and `ℝ`, although not necessary (a version in ordered fields is
+given in `filter.tendsto.const_mul_at_top`). -/
+lemma filter.tendsto.const_mul_at_top' (hr : 0 < r) (hf : tendsto f l at_top) :
+  tendsto (λx, r * f x) l at_top :=
+begin
+  apply tendsto_at_top.2 (λb, _),
+  obtain ⟨n : ℕ, hn : 1 ≤ n •ℕ r⟩ := archimedean.arch 1 hr,
+  rw nsmul_eq_mul' at hn,
+  filter_upwards [tendsto_at_top.1 hf (n * max b 0)],
+  assume x hx,
+  calc b ≤ 1 * max b 0 : by { rw [one_mul], exact le_max_left _ _ }
+  ... ≤ (r * n) * max b 0 : mul_le_mul_of_nonneg_right hn (le_max_right _ _)
+  ... = r * (n * max b 0) : by rw [mul_assoc]
+  ... ≤ r * f x : mul_le_mul_of_nonneg_left hx (le_of_lt hr)
+end
+
+/-- If a function tends to infinity along a filter, then this function multiplied by a positive
+constant (on the right) also tends to infinity. The archimedean assumption is convenient to get a
+statement that works on `ℕ`, `ℤ` and `ℝ`, although not necessary (a version in ordered fields is
+given in `filter.tendsto.at_top_mul_const`). -/
+lemma filter.tendsto.at_top_mul_const' (hr : 0 < r) (hf : tendsto f l at_top) :
+  tendsto (λx, f x * r) l at_top :=
+begin
+  apply tendsto_at_top.2 (λb, _),
+  obtain ⟨n : ℕ, hn : 1 ≤ n •ℕ r⟩ := archimedean.arch 1 hr,
+  have hn' : 1 ≤ (n : R) * r, by rwa nsmul_eq_mul at hn,
+  filter_upwards [tendsto_at_top.1 hf (max b 0 * n)],
+  assume x hx,
+  calc b ≤ max b 0 * 1 : by { rw [mul_one], exact le_max_left _ _ }
+  ... ≤ max b 0 * (n * r) : mul_le_mul_of_nonneg_left hn' (le_max_right _ _)
+  ... = (max b 0 * n) * r : by rw [mul_assoc]
+  ... ≤ f x * r : mul_le_mul_of_nonneg_right hx (le_of_lt hr)
+end

src/order/filter/at_top_bot.lean

@@ -385,6 +385,17 @@ lemma tendsto_at_bot_add (hf : tendsto f l at_bot) (hg : tendsto g l at_bot) :
   tendsto (λ x, f x + g x) l at_bot :=
 @tendsto_at_top_add _ (order_dual β) _ _ _ _ hf hg
 
+lemma tendsto.nsmul_at_top (hf : tendsto f l at_top) {n : ℕ} (hn : 0 < n) :
+  tendsto (λ x, n •ℕ f x) l at_top :=
+tendsto_at_top.2 $ λ y, (tendsto_at_top.1 hf y).mp $ (tendsto_at_top.1 hf 0).mono $ λ x h₀ hy,
+calc y ≤ f x : hy
+... = 1 •ℕ f x : (one_nsmul _).symm
+... ≤  n •ℕ f x : nsmul_le_nsmul h₀ hn
+
+lemma tendsto.nsmul_at_bot (hf : tendsto f l at_bot) {n : ℕ} (hn : 0 < n) :
+  tendsto (λ x, n •ℕ f x) l at_bot :=
+@tendsto.nsmul_at_top α (order_dual β) _ l f hf n hn
+
 end ordered_add_comm_monoid
 
 section ordered_cancel_add_comm_monoid
@@ -501,22 +512,150 @@ lemma tendsto_at_bot_add_const_right (C : β) (hf : tendsto f l at_bot) :
   tendsto (λ x, f x + C) l at_bot :=
 @tendsto_at_top_add_const_right _ (order_dual β) _ _ _ C hf
 
+lemma tendsto_neg_at_top_at_bot : tendsto (has_neg.neg : β → β) at_top at_bot :=
+begin
+  simp only [tendsto_at_bot, neg_le],
+  exact λ b, eventually_ge_at_top _
+end
+
+lemma tendsto_neg_at_bot_at_top : tendsto (has_neg.neg : β → β) at_bot at_top :=
+@tendsto_neg_at_top_at_bot (order_dual β) _
+
 end ordered_group
 
-section linear_ordered_semiring
+section ordered_semiring
 
 variables [ordered_semiring α] {l : filter β} {f g : β → α}
 
-lemma tendsto_at_top_mul_at_top (hf : tendsto f l at_top) (hg : tendsto g l at_top) :
+lemma tendsto.at_top_mul_at_top (hf : tendsto f l at_top) (hg : tendsto g l at_top) :
   tendsto (λ x, f x * g x) l at_top :=
 begin
   refine tendsto_at_top_mono' _ _ hg,
-  filter_upwards [hg (eventually_ge_at_top 0), hf (eventually_ge_at_top 1)],
+  filter_upwards [hg.eventually (eventually_ge_at_top 0), hf.eventually (eventually_ge_at_top 1)],
   exact λ x, le_mul_of_one_le_left
 end
 
+lemma tendsto_mul_self_at_top : tendsto (λ x : α, x * x) at_top at_top :=
+tendsto_id.at_top_mul_at_top tendsto_id
+
+/-- The function `x^n` tends to `+∞` at `+∞` for any positive natural `n`.
+A version for positive real powers exists as `tendsto_rpow_at_top`. -/
+lemma tendsto_pow_at_top {n : ℕ} (hn : 1 ≤ n) : tendsto (λ x : α, x ^ n) at_top at_top :=
+begin
+  refine tendsto_at_top_mono' _ ((eventually_ge_at_top 1).mono $ λ x hx, _) tendsto_id,
+  simpa only [pow_one] using pow_le_pow hx hn
+end
+
+end ordered_semiring
+
+section ordered_ring
+
+variables [ordered_ring α] {l : filter β} {f g : β → α}
+
+lemma tendsto.at_top_mul_at_bot (hf : tendsto f l at_top) (hg : tendsto g l at_bot) :
+  tendsto (λ x, f x * g x) l at_bot :=
+have _ := (hf.at_top_mul_at_top $ tendsto_neg_at_bot_at_top.comp hg),
+by simpa only [(∘), neg_mul_eq_mul_neg, neg_neg] using tendsto_neg_at_top_at_bot.comp this
+
+lemma tendsto.at_bot_mul_at_top (hf : tendsto f l at_bot) (hg : tendsto g l at_top) :
+  tendsto (λ x, f x * g x) l at_bot :=
+have tendsto (λ x, (-f x) * g x) l at_top :=
+  ( (tendsto_neg_at_bot_at_top.comp hf).at_top_mul_at_top hg),
+by simpa only [(∘), neg_mul_eq_neg_mul, neg_neg] using tendsto_neg_at_top_at_bot.comp this
+
+lemma tendsto.at_bot_mul_at_bot (hf : tendsto f l at_bot) (hg : tendsto g l at_bot) :
+  tendsto (λ x, f x * g x) l at_top :=
+have tendsto (λ x, (-f x) * (-g x)) l at_top :=
+  (tendsto_neg_at_bot_at_top.comp hf).at_top_mul_at_top (tendsto_neg_at_bot_at_top.comp hg),
+by simpa only [neg_mul_neg] using this
+
+end ordered_ring
+
+section linear_ordered_semiring
+
+variables [linear_ordered_semiring α] {l : filter β} {f : β → α}
+
+lemma tendsto.at_top_of_const_mul {c : α} (hc : 0 < c) (hf : tendsto (λ x, c * f x) l at_top) :
+  tendsto f l at_top :=
+tendsto_at_top.2 $ λ b, (tendsto_at_top.1 hf (c * b)).mono $ λ x hx, le_of_mul_le_mul_left hx hc
+
+lemma tendsto.at_top_of_mul_const {c : α} (hc : 0 < c) (hf : tendsto (λ x, f x * c) l at_top) :
+  tendsto f l at_top :=
+tendsto_at_top.2 $ λ b, (tendsto_at_top.1 hf (b * c)).mono $ λ x hx, le_of_mul_le_mul_right hx hc
+
 end linear_ordered_semiring
 
+section linear_ordered_field
+
+variables [linear_ordered_field α] {l : filter β} {f : β → α} {r : α}
+
+/-- If a function tends to infinity along a filter, then this function multiplied by a positive
+constant (on the left) also tends to infinity. For a version working in `ℕ` or `ℤ`, use
+`filter.tendsto.const_mul_at_top'` instead. -/
+lemma tendsto.const_mul_at_top (hr : 0 < r) (hf : tendsto f l at_top) :
+  tendsto (λx, r * f x) l at_top :=
+tendsto.at_top_of_const_mul (inv_pos.2 hr) $ by simpa only [inv_mul_cancel_left' hr.ne']
+
+/-- If a function tends to infinity along a filter, then this function multiplied by a positive
+constant (on the right) also tends to infinity. For a version working in `ℕ` or `ℤ`, use
+`filter.tendsto.at_top_mul_const'` instead. -/
+lemma tendsto.at_top_mul_const (hr : 0 < r) (hf : tendsto f l at_top) :
+  tendsto (λx, f x * r) l at_top :=
+by simpa only [mul_comm] using hf.const_mul_at_top hr
+
+/-- If a function tends to infinity along a filter, then this function divided by a positive
+constant also tends to infinity. -/
+lemma tendsto.at_top_div_const (hr : 0 < r) (hf : tendsto f l at_top) :
+  tendsto (λx, f x / r) l at_top :=
+hf.at_top_mul_const (inv_pos.2 hr)
+
+/-- If a function tends to infinity along a filter, then this function multiplied by a negative
+constant (on the left) tends to negative infinity. -/
+lemma tendsto.neg_const_mul_at_top (hr : r < 0) (hf : tendsto f l at_top) :
+  tendsto (λ x, r * f x) l at_bot :=
+by simpa only [(∘), neg_mul_eq_neg_mul, neg_neg]
+  using tendsto_neg_at_top_at_bot.comp (hf.const_mul_at_top (neg_pos.2 hr))
+
+/-- If a function tends to infinity along a filter, then this function multiplied by a negative
+constant (on the right) tends to negative infinity. -/
+lemma tendsto.at_top_mul_neg_const (hr : r < 0) (hf : tendsto f l at_top) :
+  tendsto (λ x, f x * r) l at_bot :=
+by simpa only [mul_comm] using hf.neg_const_mul_at_top hr
+
+/-- If a function tends to negative infinity along a filter, then this function multiplied by
+a positive constant (on the left) also tends to negative infinity. -/
+lemma tendsto.const_mul_at_bot (hr : 0 < r) (hf : tendsto f l at_bot) :
+  tendsto (λx, r * f x) l at_bot :=
+by simpa only [(∘), neg_mul_eq_mul_neg, neg_neg]
+  using tendsto_neg_at_top_at_bot.comp ((tendsto_neg_at_bot_at_top.comp hf).const_mul_at_top hr)
+
+/-- If a function tends to negative infinity along a filter, then this function multiplied by
+a positive constant (on the right) also tends to negative infinity. -/
+lemma tendsto.at_bot_mul_const (hr : 0 < r) (hf : tendsto f l at_bot) :
+  tendsto (λx, f x * r) l at_bot :=
+by simpa only [mul_comm] using hf.const_mul_at_bot hr
+
+/-- If a function tends to negative infinity along a filter, then this function divided by
+a positive constant also tends to negative infinity. -/
+lemma tendsto.at_bot_div_const (hr : 0 < r) (hf : tendsto f l at_bot) :
+  tendsto (λx, f x / r) l at_bot :=
+hf.at_bot_mul_const (inv_pos.2 hr)
+
+/-- If a function tends to negative infinity along a filter, then this function multiplied by
+a negative constant (on the left) tends to positive infinity. -/
+lemma tendsto.neg_const_mul_at_bot (hr : r < 0) (hf : tendsto f l at_bot) :
+  tendsto (λ x, r * f x) l at_top :=
+by simpa only [(∘), neg_mul_eq_neg_mul, neg_neg]
+  using tendsto_neg_at_bot_at_top.comp (hf.const_mul_at_bot (neg_pos.2 hr))
+
+/-- If a function tends to negative infinity along a filter, then this function multiplied by
+a negative constant (on the right) tends to positive infinity. -/
+lemma tendsto.at_bot_mul_neg_const (hr : r < 0) (hf : tendsto f l at_bot) :
+  tendsto (λ x, f x * r) l at_top :=
+by simpa only [mul_comm] using hf.neg_const_mul_at_bot hr
+
+end linear_ordered_field
+
 open_locale filter
 
 lemma tendsto_at_top' [nonempty α] [semilattice_sup α] {f : α → β} {l : filter β} :
@@ -909,17 +1048,6 @@ lemma tendsto_at_bot_of_monotone_of_subseq [preorder ι] [preorder α] {u : ι 
   tendsto u at_bot at_bot :=
 tendsto_at_bot_of_monotone_of_filter h (tendsto_map' H)
 
-lemma tendsto_neg_at_top_at_bot [ordered_add_comm_group α] :
-  tendsto (has_neg.neg : α → α) at_top at_bot :=
-begin
-  simp only [tendsto_at_bot, neg_le],
-  exact λ b, eventually_ge_at_top _
-end
-
-lemma tendsto_neg_at_bot_at_top [ordered_add_comm_group α] :
-  tendsto (has_neg.neg : α → α) at_bot at_top :=
-@tendsto_neg_at_top_at_bot (order_dual α) _
-
 /-- Let `f` and `g` be two maps to the same commutative monoid. This lemma gives a sufficient
 condition for comparison of the filter `at_top.map (λ s, ∏ b in s, f b)` with
 `at_top.map (λ s, ∏ b in s, g b)`. This is useful to compare the set of limit points of