feat(special_functions/polynomials): Generalize some polynomial asymp…

…totics to iff statements. (#7545)

src/analysis/asymptotics/asymptotic_equivalent.lean

@@ -105,6 +105,13 @@ begin
   exact is_o_zero_right_iff
 end
 
+lemma is_equivalent_zero_iff_is_O_zero : u ~[l] 0 ↔ is_O u (0 : α → β) l :=
+begin
+  refine ⟨is_equivalent.is_O, λ h, _⟩,
+  rw [is_equivalent_zero_iff_eventually_zero, eventually_eq_iff_exists_mem],
+  exact ⟨{x : α | u x = 0}, is_O_zero_right_iff.mp h, λ x hx, hx⟩,
+end
+
 lemma is_equivalent_const_iff_tendsto {c : β} (h : c ≠ 0) : u ~[l] const _ c ↔ tendsto u l (𝓝 c) :=
 begin
   rw [is_equivalent, is_o_const_iff h],

src/analysis/special_functions/polynomials.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anatole Dedecker
+Authors: Anatole Dedecker, Devon Tuma
 -/
 import analysis.asymptotics.asymptotic_equivalent
 import analysis.asymptotics.specific_asymptotics
@@ -29,13 +29,15 @@ variables {𝕜 : Type*} [normed_linear_ordered_field 𝕜] (P Q : polynomial 
 
 lemma eventually_no_roots (hP : P ≠ 0) : ∀ᶠ x in filter.at_top, ¬ P.is_root x :=
 begin
-  obtain ⟨x₀, hx₀⟩ := polynomial.exists_max_root P hP,
+  obtain ⟨x₀, hx₀⟩ := exists_max_root P hP,
   refine filter.eventually_at_top.mpr (⟨x₀ + 1, λ x hx h, _⟩),
   exact absurd (hx₀ x h) (not_le.mpr (lt_of_lt_of_le (lt_add_one x₀) hx)),
 end
 
 variables [order_topology 𝕜]
 
+section polynomial_at_top
+
 lemma is_equivalent_at_top_lead :
   (λ x, eval x P) ~[at_top] (λ x, P.leading_coeff * x ^ P.nat_degree) :=
 begin
@@ -55,12 +57,34 @@ P.is_equivalent_at_top_lead.symm.tendsto_at_top
   (tendsto_const_mul_pow_at_top (le_nat_degree_of_coe_le_degree hdeg)
     (lt_of_le_of_ne hnng $ ne.symm $ mt leading_coeff_eq_zero.mp $ ne_zero_of_coe_le_degree hdeg))
 
+lemma tendsto_at_top_iff_leading_coeff_nonneg :
+  tendsto (λ x, eval x P) at_top at_top ↔ 1 ≤ P.degree ∧ 0 ≤ P.leading_coeff :=
+begin
+  refine ⟨λ h, _, λ h, tendsto_at_top_of_leading_coeff_nonneg P h.1 h.2⟩,
+  have : tendsto (λ x, P.leading_coeff * x ^ P.nat_degree) at_top at_top :=
+    is_equivalent.tendsto_at_top (is_equivalent_at_top_lead P) h,
+  rw tendsto_const_mul_pow_at_top_iff P.leading_coeff P.nat_degree at this,
+  rw [degree_eq_nat_degree (leading_coeff_ne_zero.mp (ne_of_lt this.2).symm), ← nat.cast_one],
+  refine ⟨with_bot.coe_le_coe.mpr this.1, le_of_lt this.2⟩,
+end
+
 lemma tendsto_at_bot_of_leading_coeff_nonpos (hdeg : 1 ≤ P.degree) (hnps : P.leading_coeff ≤ 0) :
   tendsto (λ x, eval x P) at_top at_bot :=
 P.is_equivalent_at_top_lead.symm.tendsto_at_bot
   (tendsto_neg_const_mul_pow_at_top (le_nat_degree_of_coe_le_degree hdeg)
     (lt_of_le_of_ne hnps $ mt leading_coeff_eq_zero.mp $ ne_zero_of_coe_le_degree hdeg))
 
+lemma tendsto_at_bot_iff_leading_coeff_nonpos :
+  tendsto (λ x, eval x P) at_top at_bot ↔ 1 ≤ P.degree ∧ P.leading_coeff ≤ 0 :=
+begin
+  refine ⟨λ h, _, λ h, tendsto_at_bot_of_leading_coeff_nonpos P h.1 h.2⟩,
+  have : tendsto (λ x, P.leading_coeff * x ^ P.nat_degree) at_top at_bot :=
+    (is_equivalent.tendsto_at_bot (is_equivalent_at_top_lead P) h),
+  rw tendsto_neg_const_mul_pow_at_top_iff P.leading_coeff P.nat_degree at this,
+  rw [degree_eq_nat_degree (leading_coeff_ne_zero.mp (ne_of_lt this.2)), ← nat.cast_one],
+  refine ⟨with_bot.coe_le_coe.mpr this.1, le_of_lt this.2⟩,
+end
+
 lemma abs_tendsto_at_top (hdeg : 1 ≤ P.degree) :
   tendsto (λ x, abs $ eval x P) at_top at_top :=
 begin
@@ -70,6 +94,42 @@ begin
     exact tendsto_abs_at_bot_at_top.comp (P.tendsto_at_bot_of_leading_coeff_nonpos hdeg hP.le)}
 end
 
+lemma abs_is_bounded_under_iff :
+  is_bounded_under (≤) at_top (λ x, abs (eval x P)) ↔ P.degree ≤ 0 :=
+begin
+  refine ⟨λ h, _, λ h, ⟨abs (P.coeff 0), eventually_map.mpr (eventually_of_forall
+    (forall_imp (λ _, le_of_eq) (λ x, congr_arg abs $ trans (congr_arg (eval x)
+    (eq_C_of_degree_le_zero h)) (eval_C))))⟩⟩,
+  contrapose! h,
+  exact not_is_bounded_under_of_tendsto_at_top
+    (abs_tendsto_at_top P (nat.with_bot.one_le_iff_zero_lt.2 h))
+end
+
+lemma abs_tendsto_at_top_iff :
+  tendsto (λ x, abs $ eval x P) at_top at_top ↔ 1 ≤ P.degree :=
+⟨λ h, nat.with_bot.one_le_iff_zero_lt.2 (not_le.mp ((mt (abs_is_bounded_under_iff P).mpr)
+  (not_is_bounded_under_of_tendsto_at_top h))), abs_tendsto_at_top P⟩
+
+lemma tendsto_nhds_iff {c : 𝕜} :
+  tendsto (λ x, eval x P) at_top (𝓝 c) ↔ P.leading_coeff = c ∧ P.degree ≤ 0 :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { have := P.is_equivalent_at_top_lead.tendsto_nhds h,
+    by_cases hP : P.leading_coeff = 0,
+    { simp only [hP, zero_mul, tendsto_const_nhds_iff] at this,
+      refine ⟨trans hP this, by simp [leading_coeff_eq_zero.1 hP]⟩ },
+    { rw [tendsto_const_mul_pow_nhds_iff hP, nat_degree_eq_zero_iff_degree_le_zero] at this,
+      exact this.symm } },
+  { refine P.is_equivalent_at_top_lead.symm.tendsto_nhds _,
+    have : P.nat_degree = 0 := nat_degree_eq_zero_iff_degree_le_zero.2 h.2,
+    simp only [h.1, this, pow_zero, mul_one],
+    exact tendsto_const_nhds }
+end
+
+end polynomial_at_top
+
+section polynomial_div_at_top
+
 lemma is_equivalent_at_top_div :
   (λ x, (eval x P)/(eval x Q)) ~[at_top]
     λ x, P.leading_coeff/Q.leading_coeff * x^(P.nat_degree - Q.nat_degree : ℤ) :=
@@ -96,6 +156,24 @@ begin
   linarith
 end
 
+lemma div_tendsto_zero_iff_degree_lt (hQ : Q ≠ 0) :
+  tendsto (λ x, (eval x P)/(eval x Q)) at_top (𝓝 0) ↔ P.degree < Q.degree :=
+begin
+  refine ⟨λ h, _, div_tendsto_zero_of_degree_lt P Q⟩,
+  by_cases hPQ : P.leading_coeff / Q.leading_coeff = 0,
+  { simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ,
+    cases hPQ with hP0 hQ0,
+    { rw [leading_coeff_eq_zero.1 hP0, degree_zero],
+      exact bot_lt_iff_ne_bot.2 (λ hQ', hQ (degree_eq_bot.1 hQ')) },
+    { exact absurd (leading_coeff_eq_zero.1 hQ0) hQ } },
+  { have := (is_equivalent_at_top_div P Q).tendsto_nhds h,
+    rw tendsto_const_mul_fpow_at_top_zero_iff hPQ at this,
+    cases this with h h,
+    { exact absurd h.2 hPQ },
+    { rw [sub_lt_iff_lt_add, zero_add, int.coe_nat_lt] at h,
+      exact degree_lt_degree h.1 } }
+end
+
 lemma div_tendsto_leading_coeff_div_of_degree_eq (hdeg : P.degree = Q.degree) :
   tendsto (λ x, (eval x P)/(eval x Q)) at_top (𝓝 $ P.leading_coeff / Q.leading_coeff) :=
 begin
@@ -146,7 +224,7 @@ have ratio_neg : P.leading_coeff/Q.leading_coeff < 0,
       (λ h, hQ $ leading_coeff_eq_zero.mp h)),
 div_tendsto_at_bot_of_degree_gt' P Q hdeg ratio_neg
 
-lemma eval_div_tendsto_at_top_of_degree_gt (hdeg : Q.degree < P.degree)
+lemma abs_div_tendsto_at_top_of_degree_gt (hdeg : Q.degree < P.degree)
   (hQ : Q ≠ 0) :
   tendsto (λ x, abs ((eval x P)/(eval x Q))) at_top at_top :=
 begin
@@ -156,6 +234,8 @@ begin
     exact tendsto_abs_at_bot_at_top.comp (P.div_tendsto_at_bot_of_degree_gt Q hdeg hQ h.le) }
 end
 
+end polynomial_div_at_top
+
 theorem is_O_of_degree_le (h : P.degree ≤ Q.degree) :
   is_O (λ x, eval x P) (λ x, eval x Q) filter.at_top :=
 begin

src/data/nat/with_bot.lean

@@ -38,4 +38,12 @@ by rw [← with_bot.coe_zero, with_bot.coe_le_coe]; exact nat.zero_le _
 option.cases_on n dec_trivial (λ n, iff_of_false
   (by simp [with_bot.some_eq_coe]) (λ h, option.no_confusion h))
 
+lemma with_bot.one_le_iff_zero_lt {x : with_bot ℕ} : 1 ≤ x ↔ 0 < x :=
+begin
+  refine ⟨λ h, lt_of_lt_of_le (with_bot.coe_lt_coe.mpr zero_lt_one) h, λ h, _⟩,
+  induction x using with_bot.rec_bot_coe,
+  { exact false.elim (not_lt_of_lt (with_bot.bot_lt_some 0) h) },
+  { exact with_bot.coe_le_coe.mpr (nat.succ_le_iff.mpr (with_bot.coe_lt_coe.mp h)) }
+end
+
 end nat

src/order/filter/at_top_bot.lean

@@ -724,10 +724,39 @@ lemma tendsto_const_mul_pow_at_top {c : α} {n : ℕ}
   (hn : 1 ≤ n) (hc : 0 < c) : tendsto (λ x, c * x^n) at_top at_top :=
 tendsto.const_mul_at_top hc (tendsto_pow_at_top hn)
 
+lemma tendsto_const_mul_pow_at_top_iff (c : α) (n : ℕ) :
+  tendsto (λ x, c * x^n) at_top at_top ↔ 1 ≤ n ∧ 0 < c :=
+begin
+  refine ⟨λ h, _, λ h, tendsto_const_mul_pow_at_top h.1 h.2⟩,
+  simp only [tendsto_at_top, eventually_at_top] at h,
+  have : 0 < c := let ⟨x, hx⟩ := h 1 in
+    pos_of_mul_pos_right (lt_of_lt_of_le zero_lt_one (hx (max x 1) (le_max_left x 1)))
+    (pow_nonneg (le_trans zero_le_one (le_max_right x 1)) n),
+  refine ⟨nat.succ_le_iff.mp (lt_of_le_of_ne (zero_le n) (ne.symm (λ hn, _))), this⟩,
+  obtain ⟨x, hx⟩ := h (c + 1),
+  specialize hx x le_rfl,
+  rw [hn, pow_zero, mul_one, add_le_iff_nonpos_right] at hx,
+  exact absurd hx (not_le.mpr zero_lt_one),
+end
+
 lemma tendsto_neg_const_mul_pow_at_top {c : α} {n : ℕ}
   (hn : 1 ≤ n) (hc : c < 0) : tendsto (λ x, c * x^n) at_top at_bot :=
 tendsto.neg_const_mul_at_top hc (tendsto_pow_at_top hn)
 
+lemma tendsto_neg_const_mul_pow_at_top_iff (c : α) (n : ℕ) :
+  tendsto (λ x, c * x^n) at_top at_bot ↔ 1 ≤ n ∧ c < 0 :=
+begin
+  refine ⟨λ h, _, λ h, tendsto_neg_const_mul_pow_at_top h.1 h.2⟩,
+  simp only [tendsto_at_bot, eventually_at_top] at h,
+  have : c < 0 := let ⟨x, hx⟩ := h (-1) in
+    neg_of_mul_neg_right (lt_of_le_of_lt (hx (max x 1) (le_max_left x 1)) (by simp [zero_lt_one]))
+    (pow_nonneg (le_trans zero_le_one (le_max_right x 1)) n),
+  refine ⟨nat.succ_le_iff.mp (lt_of_le_of_ne (zero_le n) (ne.symm (λ hn, _))), this⟩,
+  obtain ⟨x, hx⟩ := h (c - 1),
+  specialize hx x le_rfl,
+  rw [hn, pow_zero, mul_one, le_sub, sub_self] at hx,
+  exact absurd hx (not_le.mpr zero_lt_one),
+end
 
 end linear_ordered_field
 

src/order/liminf_limsup.lean

@@ -90,6 +90,32 @@ lemma is_bounded.is_bounded_under {q : β → β → Prop} {u : α → β}
   (hf : ∀a₀ a₁, r a₀ a₁ → q (u a₀) (u a₁)) : f.is_bounded r → f.is_bounded_under q u
 | ⟨b, h⟩ := ⟨u b, show ∀ᶠ x in f, q (u x) (u b), from h.mono (λ x, hf x b)⟩
 
+lemma not_is_bounded_under_of_tendsto_at_top [nonempty α] [semilattice_sup α]
+  [preorder β] [no_top_order β] {f : α → β} (hf : tendsto f at_top at_top) :
+  ¬ is_bounded_under (≤) at_top f :=
+begin
+  rintro ⟨b, hb⟩,
+  rw eventually_map at hb,
+  obtain ⟨b', h⟩ := no_top b,
+  have hb' := (tendsto_at_top.mp hf) b',
+  have : {x : α | f x ≤ b} ∩ {x : α | b' ≤ f x} = ∅ :=
+    eq_empty_of_subset_empty (λ x hx, (not_le_of_lt h) (le_trans hx.2 hx.1)),
+  exact at_top.empty_nmem_sets (this ▸ filter.inter_mem_sets hb hb' : ∅ ∈ (at_top : filter α)),
+end
+
+lemma not_is_bounded_under_of_tendsto_at_bot [nonempty α] [semilattice_sup α]
+  [preorder β] [no_bot_order β] {f : α → β} (hf : tendsto f at_top at_bot) :
+  ¬ is_bounded_under (≥) at_top f :=
+begin
+  rintro ⟨b, hb⟩,
+  rw eventually_map at hb,
+  obtain ⟨b', h⟩ := no_bot b,
+  have hb' := (tendsto_at_bot.mp hf) b',
+  have : {x : α | b ≤ f x} ∩ {x : α | f x ≤ b'} = ∅ :=
+    eq_empty_of_subset_empty (λ x hx, (not_le_of_lt h) (le_trans hx.1 hx.2)),
+  exact at_top.empty_nmem_sets (this ▸ filter.inter_mem_sets hb hb' : ∅ ∈ (at_top : filter α)),
+end
+
 /-- `is_cobounded (≺) f` states that the filter `f` does not tend to infinity w.r.t. `≺`. This is
 also called frequently bounded. Will be usually instantiated with `≤` or `≥`.