feat(analysis): prove that a polynomial function is equivalent to its…

… leading term along at_top, and consequences (#5354)

The main result is `eval_is_equivalent_at_top_eval_lead`, which states that for
any polynomial `P` of degree `n` with leading coeff `a`, the corresponding polynomial
function is equivalent to `a * x^n` as `x` goes to +∞.
We can then use this result to prove various limits for polynomial and rational
functions, depending on the degrees and leading coeffs of the considered polynomials.



Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/analysis/asymptotic_equivalent.lean → src/analysis/asymptotics/asymptotic_equivalent.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import analysis.asymptotics
+import analysis.asymptotics.asymptotics
 import analysis.normed_space.ordered
 import analysis.normed_space.bounded_linear_maps
 
@@ -91,6 +91,14 @@ end
 @[trans] lemma is_equivalent.trans (huv : u ~[l] v) (hvw : v ~[l] w) : u ~[l] w :=
 (huv.is_o.trans_is_O hvw.is_O).triangle hvw.is_o
 
+lemma is_equivalent.congr_left {u v w : α → β} {l : filter α} (huv : u ~[l] v)
+  (huw : u =ᶠ[l] w) : w ~[l] v :=
+is_o.congr' (huw.sub (eventually_eq.refl _ _)) (eventually_eq.refl _ _) huv
+
+lemma is_equivalent.congr_right {u v w : α → β} {l : filter α} (huv : u ~[l] v)
+  (hvw : v =ᶠ[l] w) : u ~[l] w :=
+(huv.symm.congr_left hvw).symm
+
 lemma is_equivalent_zero_iff_eventually_zero : u ~[l] 0 ↔ u =ᶠ[l] 0 :=
 begin
   rw [is_equivalent, sub_zero],
@@ -127,6 +135,24 @@ end
 lemma is_equivalent.tendsto_nhds_iff {c : β} (huv : u ~[l] v) :
   tendsto u l (𝓝 c) ↔ tendsto v l (𝓝 c) := ⟨huv.tendsto_nhds, huv.symm.tendsto_nhds⟩
 
+lemma is_equivalent.add_is_o (huv : u ~[l] v) (hwv : is_o w v l) : (w + u) ~[l] v :=
+begin
+  rw is_equivalent at *,
+  convert hwv.add huv,
+  ext,
+  simp [add_sub],
+end
+
+lemma is_o.is_equivalent (huv : is_o (u - v) v l) : u ~[l] v := huv
+
+lemma is_equivalent.neg (huv : u ~[l] v) : (λ x, - u x) ~[l] (λ x, - v x) :=
+begin
+  rw is_equivalent,
+  convert huv.is_o.neg_left.neg_right,
+  ext,
+  simp,
+end
+
 end normed_group
 
 open_locale asymptotics
@@ -256,6 +282,26 @@ 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⟩
 
+lemma is_equivalent.tendsto_at_bot [order_topology β] (huv : u ~[l] v) (hu : tendsto u l at_bot) :
+  tendsto v l at_bot :=
+begin
+  convert tendsto_neg_at_top_at_bot.comp
+    (huv.neg.tendsto_at_top $ tendsto_neg_at_bot_at_top.comp hu),
+  ext,
+  simp
+end
+
+lemma is_equivalent.tendsto_at_bot_iff [order_topology β] (huv : u ~[l] v) :
+  tendsto u l at_bot ↔ tendsto v l at_bot := ⟨huv.tendsto_at_bot, huv.symm.tendsto_at_bot⟩
+
 end normed_linear_ordered_field
 
 end asymptotics
+
+open filter asymptotics
+open_locale asymptotics
+
+variables {α β : Type*} [normed_group β]
+
+lemma filter.eventually_eq.is_equivalent {u v : α → β} {l : filter α} (h : u =ᶠ[l] v) : u ~[l] v :=
+is_o.congr' h.sub_eq.symm (eventually_eq.refl _ _) (is_o_zero v l)

src/analysis/asymptotics.lean → src/analysis/asymptotics/asymptotics.lean

@@ -1238,6 +1238,15 @@ end exists_mul_eq
 
 /-! ### Miscellanous lemmas -/
 
+lemma is_o.tendsto_zero_of_tendsto {α E 𝕜 : Type*} [normed_group E] [normed_field 𝕜] {u : α → E}
+  {v : α → 𝕜} {l : filter α} {y : 𝕜} (huv : is_o u v l) (hv : tendsto v l (𝓝 y)) :
+  tendsto u l (𝓝 0) :=
+begin
+  suffices h : is_o u (λ x, (1 : 𝕜)) l,
+  { rwa is_o_one_iff at h },
+  exact huv.trans_is_O (is_O_one_of_tendsto 𝕜 hv),
+end
+
 theorem is_o_pow_pow {m n : ℕ} (h : m < n) :
   is_o (λ(x : 𝕜), x^n) (λx, x^m) (𝓝 0) :=
 begin

src/analysis/asymptotics/specific_asymptotics.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2021 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+import analysis.normed_space.ordered
+import analysis.asymptotics.asymptotics
+
+/-!
+# A collection of specific asymptotic results
+
+This file contains specific lemmas about asymptotics which don't have their place in the general
+theory developped in `analysis.asymptotics.asymptotics`.
+-/
+
+open filter asymptotics
+open_locale topological_space
+
+section linear_ordered_field
+
+variables {𝕜 : Type*} [linear_ordered_field 𝕜]
+
+lemma pow_div_pow_eventually_eq_at_top {p q : ℕ} :
+  (λ x : 𝕜, x^p / x^q) =ᶠ[at_top] (λ x, x^((p : ℤ) -q)) :=
+begin
+  apply ((eventually_gt_at_top (0 : 𝕜)).mono (λ x hx, _)),
+  simp [fpow_sub hx.ne'],
+end
+
+lemma pow_div_pow_eventually_eq_at_bot {p q : ℕ} :
+  (λ x : 𝕜, x^p / x^q) =ᶠ[at_bot] (λ x, x^((p : ℤ) -q)) :=
+begin
+  apply ((eventually_lt_at_bot (0 : 𝕜)).mono (λ x hx, _)),
+  simp [fpow_sub hx.ne'.symm],
+end
+
+lemma tendsto_fpow_at_top_at_top {n : ℤ}
+  (hn : 0 < n) : tendsto (λ x : 𝕜, x^n) at_top at_top :=
+begin
+  lift n to ℕ using hn.le,
+  exact tendsto_pow_at_top (nat.succ_le_iff.mpr $int.coe_nat_pos.mp hn)
+end
+
+lemma tendsto_pow_div_pow_at_top_at_top {p q : ℕ}
+  (hpq : q < p) : tendsto (λ x : 𝕜, x^p / x^q) at_top at_top :=
+begin
+  rw tendsto_congr' pow_div_pow_eventually_eq_at_top,
+  apply tendsto_fpow_at_top_at_top,
+  linarith
+end
+
+lemma tendsto_pow_div_pow_at_top_zero [topological_space 𝕜] [order_topology 𝕜] {p q : ℕ}
+  (hpq : p < q) : tendsto (λ x : 𝕜, x^p / x^q) at_top (𝓝 0) :=
+begin
+  rw tendsto_congr' pow_div_pow_eventually_eq_at_top,
+  apply tendsto_fpow_at_top_zero,
+  linarith
+end
+
+end linear_ordered_field
+
+section normed_linear_ordered_field
+
+variables {𝕜 : Type*} [normed_linear_ordered_field 𝕜]
+
+lemma asymptotics.is_o_pow_pow_at_top_of_lt
+  [order_topology 𝕜] {p q : ℕ} (hpq : p < q) :
+  is_o (λ x : 𝕜, x^p) (λ x, x^q) at_top :=
+begin
+  refine (is_o_iff_tendsto' _).mpr (tendsto_pow_div_pow_at_top_zero hpq),
+  exact (eventually_gt_at_top 0).mono (λ x hx hxq, (pow_ne_zero q hx.ne' hxq).elim),
+end
+
+lemma asymptotics.is_O.trans_tendsto_norm_at_top {α : Type*} {u v : α → 𝕜} {l : filter α}
+  (huv : is_O u v l) (hu : tendsto (λ x, ∥u x∥) l at_top) : tendsto (λ x, ∥v x∥) l at_top :=
+begin
+  rcases huv.exists_pos with ⟨c, hc, hcuv⟩,
+  rw is_O_with at hcuv,
+  convert tendsto.at_top_div_const hc (tendsto_at_top_mono' l hcuv hu),
+  ext x,
+  rw mul_div_cancel_left _ hc.ne.symm,
+end
+
+end normed_linear_ordered_field

src/analysis/calculus/fderiv.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov
 -/
 import analysis.calculus.tangent_cone
 import analysis.normed_space.units
-import analysis.asymptotic_equivalent
+import analysis.asymptotics.asymptotic_equivalent
 import analysis.analytic.basic
 
 /-!

src/analysis/normed_space/operator_norm.lean

@@ -6,7 +6,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 import linear_algebra.finite_dimensional
 import analysis.normed_space.linear_isometry
 import analysis.normed_space.riesz_lemma
-import analysis.asymptotics
+import analysis.asymptotics.asymptotics
 
 /-!
 # Operator norm on the space of continuous linear maps

src/analysis/normed_space/ordered.lean

@@ -5,7 +5,6 @@ Authors: Anatole Dedecker
 -/
 import analysis.normed_space.basic
 import algebra.ring.basic
-import analysis.asymptotics
 
 /-!
 # Ordered normed spaces
@@ -14,7 +13,7 @@ In this file, we define classes for fields and groups that are both normed and o
 These are mostly useful to avoid diamonds during type class inference.
 -/
 
-open filter asymptotics set
+open filter set
 open_locale topological_space
 
 /-- A `normed_linear_ordered_group` is an additive group that is both a `normed_group` and
@@ -43,22 +42,10 @@ extends linear_ordered_field α, has_norm α, metric_space α :=
 [normed_linear_ordered_field α] : normed_linear_ordered_group α :=
 ⟨normed_linear_ordered_field.dist_eq⟩
 
-lemma tendsto_pow_div_pow_at_top_of_lt {α : Type*} [normed_linear_ordered_field α]
-  [order_topology α] {p q : ℕ} (hpq : p < q) :
-  tendsto (λ (x : α), x^p / x^q) at_top (𝓝 0) :=
-begin
-  suffices h : tendsto (λ (x : α), x ^ ((p : ℤ) - q)) at_top (𝓝 0),
-  { refine h.congr' ((eventually_gt_at_top (0 : α)).mono (λ x hx, _)),
-    simp [fpow_sub hx.ne'] },
-  rw [← neg_sub, ← int.coe_nat_sub hpq.le],
-  have : 1 ≤ q - p := nat.sub_pos_of_lt hpq,
-  exact tendsto_pow_neg_at_top this
-end
+noncomputable
+instance : normed_linear_ordered_field ℚ :=
+⟨dist_eq_norm, normed_field.norm_mul⟩
 
-lemma is_o_pow_pow_at_top_of_lt {α : Type} [normed_linear_ordered_field α]
-  [order_topology α] {p q : ℕ} (hpq : p < q) :
-  is_o (λ (x : α), x^p) (λ (x : α), x^q) at_top :=
-begin
-  refine (is_o_iff_tendsto' _).mpr (tendsto_pow_div_pow_at_top_of_lt hpq),
-  exact (eventually_gt_at_top 0).mono (λ x hx hxq, (pow_ne_zero q hx.ne' hxq).elim),
-end
+noncomputable
+instance : normed_linear_ordered_field ℝ :=
+⟨dist_eq_norm, normed_field.norm_mul⟩

src/analysis/normed_space/units.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
 import analysis.specific_limits
-import analysis.asymptotics
+import analysis.asymptotics.asymptotics
 
 /-!
 # The group of units of a complete normed ring