feat(analysis/special_functions/pow): asymptotics for real powers and…

… log (#14088)

From the unit fractions project.



Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/analysis/special_functions/log/basic.lean

@@ -261,14 +261,16 @@ lemma tendsto_pow_log_div_mul_add_at_top (a b : ℝ) (n : ℕ) (ha : a ≠ 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 :=
+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
 
+lemma is_o_log_id_at_top : asymptotics.is_o log id at_top :=
+is_o_pow_log_id_at_top.congr_left (λ x, pow_one _)
+
 end real
 
 section continuity

src/analysis/special_functions/pow.lean

@@ -964,6 +964,32 @@ begin
   filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]
 end
 
+namespace asymptotics
+
+variables {α : Type*} {r c : ℝ} {l : filter α} {f g : α → ℝ}
+
+lemma is_O_with.rpow (h : is_O_with c f g l) (hc : 0 ≤ c) (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) :
+  is_O_with (c ^ r) (λ x, f x ^ r) (λ x, g x ^ r) l :=
+begin
+  apply is_O_with.of_bound,
+  filter_upwards [hg, h.bound] with x hgx hx,
+  calc |f x ^ r| ≤ |f x| ^ r         : abs_rpow_le_abs_rpow _ _
+             ... ≤ (c * |g x|) ^ r   : rpow_le_rpow (abs_nonneg _) hx hr
+             ... = c ^ r * |g x ^ r| : by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
+end
+
+lemma is_O.rpow (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) (h : is_O f g l) :
+  is_O (λ x, f x ^ r) (λ x, g x ^ r) l :=
+let ⟨c, hc, h'⟩ := h.exists_nonneg in (h'.rpow hc hr hg).is_O
+
+lemma is_o.rpow (hr : 0 < r) (hg : 0 ≤ᶠ[l] g) (h : is_o f g l) :
+  is_o (λ x, f x ^ r) (λ x, g x ^ r) l :=
+is_o.of_is_O_with $ λ c hc, ((h.forall_is_O_with (rpow_pos_of_pos hc r⁻¹)).rpow
+  (rpow_nonneg_of_nonneg hc.le _) hr.le hg).congr_const
+    (by rw [←rpow_mul hc.le, inv_mul_cancel hr.ne', rpow_one])
+
+end asymptotics
+
 open asymptotics
 
 /-- `x ^ s = o(exp(b * x))` as `x → ∞` for any real `s` and positive `b`. -/
@@ -987,6 +1013,22 @@ is_o_zpow_exp_pos_mul_at_top k hb
 lemma is_o_rpow_exp_at_top (s : ℝ) : is_o (λ x : ℝ, x ^ s) exp at_top :=
 by simpa only [one_mul] using is_o_rpow_exp_pos_mul_at_top s one_pos
 
+lemma is_o_log_rpow_at_top {r : ℝ} (hr : 0 < r) : is_o log (λ x, x ^ r) at_top :=
+begin
+  rw ←is_o_const_mul_left_iff hr.ne',
+  refine (is_o_log_id_at_top.comp_tendsto (tendsto_rpow_at_top hr)).congr' _ eventually_eq.rfl,
+  filter_upwards [eventually_gt_at_top (0 : ℝ)] with x hx using log_rpow hx _,
+end
+
+lemma is_o_log_rpow_rpow_at_top {r s : ℝ} (hr : 0 < r) (hs : 0 < s) :
+  is_o (λ x, log x ^ r) (λ x, x ^ s) at_top :=
+begin
+  refine ((is_o_log_rpow_at_top (div_pos hs hr)).rpow hr _).congr' eventually_eq.rfl _,
+  { filter_upwards [eventually_ge_at_top (0 : ℝ)] with x hx,
+    rw [← rpow_mul hx, div_mul_cancel _ hr.ne'] },
+  { exact (tendsto_rpow_at_top (div_pos hs hr)).eventually (eventually_ge_at_top 0) },
+end
+
 end limits
 
 namespace complex