From a5ffb9b0f754afd6cc34174fb8de9fc09328fe1f Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sun, 27 Feb 2022 20:07:58 +0000 Subject: [PATCH] feat(analysis/special_functions): little o behaviour of exp/log at infinity (#11840) from the unit-fractions project --- src/analysis/special_functions/exp.lean | 21 ++++++++++++++------- src/analysis/special_functions/log.lean | 13 +++++++++++++ src/analysis/special_functions/pow.lean | 2 +- 3 files changed, 28 insertions(+), 8 deletions(-) diff --git a/src/analysis/special_functions/exp.lean b/src/analysis/special_functions/exp.lean index 2cfe6cdd42dd6..16646df652146 100644 --- a/src/analysis/special_functions/exp.lean +++ b/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 diff --git a/src/analysis/special_functions/log.lean b/src/analysis/special_functions/log.lean index 13f34d8d431aa..0e8b896ccd9a6 100644 --- a/src/analysis/special_functions/log.lean +++ b/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 diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean index c590f91ff676d..77c7f1567c2bc 100644 --- a/src/analysis/special_functions/pow.lean +++ b/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 ⊢,