feat(analysis/specific_limits): add a few more limits (#1832)

* feat(analysis/specific_limits): add a few more limits

* Drop 1 lemma, generalize two others.

* Rename `tendsto_inverse_at_top_nhds_0`, fix compile

Author: urkud

src/analysis/calculus/tangent_cone.lean

@@ -95,8 +95,7 @@ lemma tangent_cone_at.lim_zero {α : Type*} (l : filter α) {c : α → 𝕜} {d
   (hc : tendsto (λn, ∥c n∥) l at_top) (hd : tendsto (λn, c n • d n) l (𝓝 y)) :
   tendsto d l (𝓝 0) :=
 begin
-  have A : tendsto (λn, ∥c n∥⁻¹) l (𝓝 0) :=
-    tendsto_inverse_at_top_nhds_0.comp hc,
+  have A : tendsto (λn, ∥c n∥⁻¹) l (𝓝 0) := tendsto_inv_at_top_zero.comp hc,
   have B : tendsto (λn, ∥c n • d n∥) l (𝓝 ∥y∥) :=
     (continuous_norm.tendsto _).comp hd,
   have C : tendsto (λn, ∥c n∥⁻¹ * ∥c n • d n∥) l (𝓝 (0 * ∥y∥)) := A.mul B,

src/analysis/complex/exponential.lean

@@ -1832,7 +1832,7 @@ end
 /-- The real exponential function tends to 0 at -infinity or, equivalently, `exp(-x)` tends to `0`
 at +infinity -/
 lemma tendsto_exp_neg_at_top_nhds_0 : tendsto (λx, exp (-x)) at_top (𝓝 0) :=
-(tendsto.comp tendsto_inverse_at_top_nhds_0 (tendsto_exp_at_top)).congr (λx, (exp_neg x).symm)
+(tendsto_inv_at_top_zero.comp (tendsto_exp_at_top)).congr (λx, (exp_neg x).symm)
 
 /-- The function `exp(x)/x^n` tends to +infinity at +infinity, for any natural number `n` -/
 lemma tendsto_exp_div_pow_at_top (n : ℕ) : tendsto (λx, exp x / x^n) at_top at_top :=
@@ -1870,7 +1870,7 @@ end
 
 /-- The function `x^n * exp(-x)` tends to `0` at +infinity, for any natural number `n`. -/
 lemma tendsto_pow_mul_exp_neg_at_top_nhds_0 (n : ℕ) : tendsto (λx, x^n * exp (-x)) at_top (𝓝 0) :=
-(tendsto_inverse_at_top_nhds_0.comp (tendsto_exp_div_pow_at_top n)).congr $ λx,
+(tendsto_inv_at_top_zero.comp (tendsto_exp_div_pow_at_top n)).congr $ λx,
   by rw [function.comp_app, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]
 
 end exp

src/analysis/specific_limits.lean

@@ -15,6 +15,9 @@ open classical function lattice filter finset metric
 
 variables {α : Type*} {β : Type*} {ι : Type*}
 
+lemma tendsto_norm_at_top_at_top : tendsto (norm : ℝ → ℝ) at_top at_top :=
+tendsto_abs_at_top_at_top
+
 /-- 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
@@ -94,6 +97,23 @@ begin
   end
 end
 
+/-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`. -/
+lemma tendsto_inv_at_top_zero' [discrete_linear_ordered_field α] [topological_space α]
+  [orderable_topology α] : tendsto (λr:α, r⁻¹) at_top (nhds_within (0 : α) (set.Ioi 0)) :=
+begin
+  assume s hs,
+  rw mem_nhds_within_Ioi_iff_exists_Ioc_subset at hs,
+  rcases hs with ⟨C, C0, hC⟩,
+  change 0 < C at C0,
+  refine filter.mem_map.2 (mem_sets_of_superset (mem_at_top C⁻¹) (λ x hx, hC _)),
+  have : 0 < x, from lt_of_lt_of_le (inv_pos C0) hx,
+  exact ⟨inv_pos this, (inv_le C0 this).1 hx⟩
+end
+
+lemma tendsto_inv_at_top_zero [discrete_linear_ordered_field α] [topological_space α]
+  [orderable_topology α] : tendsto (λr:α, r⁻¹) at_top (𝓝 0) :=
+tendsto_le_right inf_le_left tendsto_inv_at_top_zero'
+
 lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
   (∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (𝓝 r)) → summable f
 | ⟨r, hr⟩ :=
@@ -110,25 +130,21 @@ lemma tendsto_pow_at_top_at_top_of_gt_1 {r : ℝ} (h : 1 < r) :
   ⟨n, λ m hnm, le_of_lt $
     lt_of_lt_of_le hn (pow_le_pow (le_of_lt h) hnm)⟩
 
-lemma tendsto_inverse_at_top_nhds_0 : tendsto (λr:ℝ, r⁻¹) at_top (𝓝 0) :=
-tendsto_orderable_unbounded (no_top 0) (no_bot 0) $ assume l u hl hu,
-  mem_at_top_sets.mpr ⟨u⁻¹ + 1, assume b hb,
-    have u⁻¹ < b, from lt_of_lt_of_le (lt_add_of_pos_right _ zero_lt_one) hb,
-    ⟨lt_trans hl $ inv_pos $ lt_trans (inv_pos hu) this,
-    lt_of_one_div_lt_one_div hu $
-    begin
-      rw [inv_eq_one_div],
-      simp [-one_div_eq_inv, div_div_eq_mul_div, div_one],
-      simp [this]
-    end⟩⟩
+lemma lim_norm_zero' {𝕜 : Type*} [normed_group 𝕜] :
+  tendsto (norm : 𝕜 → ℝ) (nhds_within 0 {x | x ≠ 0}) (nhds_within 0 (set.Ioi 0)) :=
+lim_norm_zero.inf $ tendsto_principal_principal.2 $ λ x hx, (norm_pos_iff _).2 hx
+
+lemma normed_field.tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type*} [normed_field 𝕜] :
+  tendsto (λ x:𝕜, ∥x⁻¹∥) (nhds_within 0 {x | x ≠ 0}) at_top :=
+(tendsto_inv_zero_at_top.comp lim_norm_zero').congr $ λ x, (normed_field.norm_inv x).symm
 
 lemma tendsto_pow_at_top_nhds_0_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
   tendsto (λn:ℕ, r^n) at_top (𝓝 0) :=
 by_cases
   (assume : r = 0, (tendsto_add_at_top_iff_nat 1).mp $ by simp [pow_succ, this, tendsto_const_nhds])
   (assume : r ≠ 0,
     have tendsto (λn, (r⁻¹ ^ n)⁻¹) at_top (𝓝 0),
-      from tendsto.comp tendsto_inverse_at_top_nhds_0
+      from tendsto_inv_at_top_zero.comp
         (tendsto_pow_at_top_at_top_of_gt_1 $ one_lt_inv (lt_of_le_of_ne h₁ this.symm) h₂),
     tendsto.congr' (univ_mem_sets' $ by simp *) this)
 
@@ -162,7 +178,7 @@ tendsto_coe_nat_real_at_top_iff.1 $
   by simpa using tendsto_pow_at_top_at_top_of_gt_1 hr
 
 lemma tendsto_inverse_at_top_nhds_0_nat : tendsto (λ n : ℕ, (n : ℝ)⁻¹) at_top (𝓝 0) :=
-tendsto.comp tendsto_inverse_at_top_nhds_0 (tendsto_coe_nat_real_at_top_iff.2 tendsto_id)
+tendsto_inv_at_top_zero.comp (tendsto_coe_nat_real_at_top_iff.2 tendsto_id)
 
 lemma tendsto_const_div_at_top_nhds_0_nat (C : ℝ) : tendsto (λ n : ℕ, C / n) at_top (𝓝 0) :=
 by simpa only [mul_zero] using tendsto_const_nhds.mul tendsto_inverse_at_top_nhds_0_nat

src/topology/algebra/ordered.lean

@@ -1360,3 +1360,6 @@ tendsto_nhds_unique at_top_ne_bot (tendsto_at_top_supr_nat f hf)
 lemma infi_eq_of_tendsto {α} [topological_space α] [complete_linear_order α] [orderable_topology α]
   {f : ℕ → α} {a : α} (hf : ∀n m, n ≤ m → f m ≤ f n) : tendsto f at_top (𝓝 a) → infi f = a :=
 tendsto_nhds_unique at_top_ne_bot (tendsto_at_top_infi_nat f hf)
+
+lemma tendsto_abs_at_top_at_top [decidable_linear_ordered_comm_group α] : tendsto (abs : α → α) at_top at_top :=
+tendsto_at_top_mono _ (λ n, le_abs_self _) tendsto_id