feat(analysis/special_functions): little o behaviour of exp/log at in…

…finity (#11840)

from the unit-fractions project

src/analysis/special_functions/exp.lean

@@ -182,11 +182,14 @@ lemma tendsto_pow_mul_exp_neg_at_top_nhds_0 (n : ℕ) : tendsto (λx, x^n * exp
 (tendsto_inv_at_top_zero.comp (tendsto_exp_div_pow_at_top n)).congr $ λx,
   by rw [comp_app, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]
 
-/-- The function `(b * exp x + c) / (x ^ n)` tends to `+∞` at `+∞`, for any positive natural number
+/-- The function `(b * exp x + c) / (x ^ n)` tends to `+∞` at `+∞`, for any natural number
 `n` and any real numbers `b` and `c` such that `b` is positive. -/
-lemma tendsto_mul_exp_add_div_pow_at_top (b c : ℝ) (n : ℕ) (hb : 0 < b) (hn : 1 ≤ n) :
-  tendsto (λ x, (b * (exp x) + c) / (x^n)) at_top at_top :=
+lemma tendsto_mul_exp_add_div_pow_at_top (b c : ℝ) (n : ℕ) (hb : 0 < b) :
+  tendsto (λ x, (b * exp x + c) / x ^ n) at_top at_top :=
 begin
+  rcases n.eq_zero_or_pos with rfl | hn,
+  { simp only [pow_zero, div_one],
+    exact (tendsto_exp_at_top.const_mul_at_top hb).at_top_add tendsto_const_nhds },
   refine tendsto.congr' (eventually_eq_of_mem (Ioi_mem_at_top 0) _)
     (((tendsto_exp_div_pow_at_top n).const_mul_at_top hb).at_top_add
       ((tendsto_pow_neg_at_top hn).mul (@tendsto_const_nhds _ _ _ c _))),
@@ -195,14 +198,14 @@ begin
   ring,
 end
 
-/-- The function `(x ^ n) / (b * exp x + c)` tends to `0` at `+∞`, for any positive natural number
+/-- The function `(x ^ n) / (b * exp x + c)` tends to `0` at `+∞`, for any natural number
 `n` and any real numbers `b` and `c` such that `b` is nonzero. -/
-lemma tendsto_div_pow_mul_exp_add_at_top (b c : ℝ) (n : ℕ) (hb : 0 ≠ b) (hn : 1 ≤ n) :
-  tendsto (λ x, x^n / (b * (exp x) + c)) at_top (𝓝 0) :=
+lemma tendsto_div_pow_mul_exp_add_at_top (b c : ℝ) (n : ℕ) (hb : 0 ≠ b) :
+  tendsto (λ x, x ^ n / (b * exp x + c)) at_top (𝓝 0) :=
 begin
   have H : ∀ d e, 0 < d → tendsto (λ (x:ℝ), x^n / (d * (exp x) + e)) at_top (𝓝 0),
   { intros b' c' h,
-    convert (tendsto_mul_exp_add_div_pow_at_top b' c' n h hn).inv_tendsto_at_top ,
+    convert (tendsto_mul_exp_add_div_pow_at_top b' c' n h).inv_tendsto_at_top ,
     ext x,
     simpa only [pi.inv_apply] using inv_div.symm },
   cases lt_or_gt_of_ne hb,
@@ -252,4 +255,8 @@ lemma tendsto_comp_exp_at_bot {α : Type*} {l : filter α} {f : ℝ → α} :
   tendsto (λ x, f (exp x)) at_bot l ↔ tendsto f (𝓝[>] 0) l :=
 by rw [← map_exp_at_bot, tendsto_map'_iff]
 
+lemma is_o_pow_exp_at_top {n : ℕ} : is_o (λ x, x^n) real.exp at_top :=
+by simpa [is_o_iff_tendsto (λ x hx, ((exp_pos x).ne' hx).elim)]
+  using tendsto_div_pow_mul_exp_add_at_top 1 0 n zero_ne_one
+
 end real

src/analysis/special_functions/log.lean

@@ -259,6 +259,19 @@ begin
   simp [ha, ih hf.2, log_mul hf.1 (finset.prod_ne_zero_iff.2 hf.2)],
 end
 
+lemma tendsto_pow_log_div_mul_add_at_top (a b : ℝ) (n : ℕ) (ha : a ≠ 0) :
+  tendsto (λ x, log x ^ n / (a * x + b)) at_top (𝓝 0) :=
+((tendsto_div_pow_mul_exp_add_at_top a b n ha.symm).comp tendsto_log_at_top).congr'
+  (by filter_upwards [eventually_gt_at_top (0 : ℝ)] with x hx using by simp [exp_log hx])
+
+lemma is_o_pow_log_id_at_top {n : ℕ} :
+  asymptotics.is_o (λ x, log x ^ n) id at_top :=
+begin
+  rw asymptotics.is_o_iff_tendsto',
+  { simpa using tendsto_pow_log_div_mul_add_at_top 1 0 n one_ne_zero },
+  filter_upwards [eventually_ne_at_top (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim,
+end
+
 end real
 
 section continuity

src/analysis/special_functions/pow.lean

@@ -877,7 +877,7 @@ lemma tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 ≠ b) :
 begin
   refine tendsto.congr' _ ((tendsto_exp_nhds_0_nhds_1.comp
     (by simpa only [mul_zero, pow_one] using ((@tendsto_const_nhds _ _ _ a _).mul
-      (tendsto_div_pow_mul_exp_add_at_top b c 1 hb (by norm_num))))).comp (tendsto_log_at_top)),
+      (tendsto_div_pow_mul_exp_add_at_top b c 1 hb)))).comp tendsto_log_at_top),
   apply eventually_eq_of_mem (Ioi_mem_at_top (0:ℝ)),
   intros x hx,
   simp only [set.mem_Ioi, function.comp_app] at hx ⊢,