feat(analysis/special_functions/polynomial): polynomials are big O of polynomials of higher degree (#6714)

Author: dtumad

src/analysis/asymptotics/asymptotics.lean

@@ -1247,6 +1247,39 @@ end exists_mul_eq
 
 /-! ### Miscellanous lemmas -/
 
+theorem div_is_bounded_under_of_is_O {α : Type*} {l : filter α}
+  {f g : α → 𝕜} (h : is_O f g l) :
+  is_bounded_under (≤) l (λ x, ∥f x / g x∥) :=
+begin
+  obtain ⟨c, hc⟩ := is_O_iff.mp h,
+  refine ⟨max c 0, eventually_map.2 (filter.mem_sets_of_superset hc (λ x hx, _))⟩,
+  simp only [mem_set_of_eq, normed_field.norm_div] at ⊢ hx,
+  by_cases hgx : g x = 0,
+  { rw [hgx, norm_zero, div_zero, le_max_iff],
+    exact or.inr le_rfl },
+  { exact le_max_iff.2 (or.inl ((div_le_iff (norm_pos_iff.2 hgx)).2 hx)) }
+end
+
+theorem is_O_iff_div_is_bounded_under {α : Type*} {l : filter α}
+  {f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) :
+  is_O f g l ↔ is_bounded_under (≤) l (λ x, ∥f x / g x∥) :=
+begin
+  refine ⟨div_is_bounded_under_of_is_O, λ h, _⟩,
+  obtain ⟨c, hc⟩ := h,
+  rw filter.eventually_iff at hgf hc,
+  simp only [mem_set_of_eq, mem_map, normed_field.norm_div] at hc,
+  refine is_O_iff.2 ⟨c, filter.eventually_of_mem (inter_mem_sets hgf hc) (λ x hx, _)⟩,
+  by_cases hgx : g x = 0,
+  { simp [hx.1 hgx, hgx] },
+  { refine (div_le_iff (norm_pos_iff.2 hgx)).mp hx.2 },
+end
+
+theorem is_O_of_div_tendsto_nhds {α : Type*} {l : filter α}
+  {f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0)
+  (c : 𝕜) (H : filter.tendsto (f / g) l (𝓝 c)) :
+  is_O f g l :=
+(is_O_iff_div_is_bounded_under hgf).2 $ is_bounded_under_of_tendsto H
+
 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) :=

src/analysis/normed_space/basic.lean

@@ -226,13 +226,21 @@ calc
   ... ≤ ∥g∥ + ∥h - g∥  : norm_add_le _ _
   ... ≤ ∥g∥ + r : by { apply add_le_add_left, rw ← dist_eq_norm, exact H }
 
+lemma norm_le_norm_add_const_of_dist_le {a b : α} {c : ℝ} (h : dist a b ≤ c) :
+  ∥a∥ ≤ ∥b∥ + c :=
+norm_le_of_mem_closed_ball h
+
 lemma norm_lt_of_mem_ball {g h : α} {r : ℝ} (H : h ∈ ball g r) :
   ∥h∥ < ∥g∥ + r :=
 calc
   ∥h∥ = ∥g + (h - g)∥ : by rw [add_sub_cancel'_right]
   ... ≤ ∥g∥ + ∥h - g∥  : norm_add_le _ _
   ... < ∥g∥ + r : by { apply add_lt_add_left, rw ← dist_eq_norm, exact H }
 
+lemma norm_lt_norm_add_const_of_dist_lt {a b : α} {c : ℝ} (h : dist a b < c) :
+  ∥a∥ < ∥b∥ + c :=
+norm_lt_of_mem_ball h
+
 @[simp] lemma mem_sphere_iff_norm (v w : α) (r : ℝ) : w ∈ sphere v r ↔ ∥w - v∥ = r :=
 by simp [dist_eq_norm]
 
@@ -469,6 +477,12 @@ lemma tendsto_iff_norm_tendsto_zero {f : ι → β} {a : filter ι} {b : β} :
   tendsto f a (𝓝 b) ↔ tendsto (λ e, ∥f e - b∥) a (𝓝 0) :=
 by { convert tendsto_iff_dist_tendsto_zero, simp [dist_eq_norm] }
 
+lemma is_bounded_under_of_tendsto {l : filter ι} {f : ι → α} {c : α}
+  (h : filter.tendsto f l (𝓝 c)) : is_bounded_under (≤) l (λ x, ∥f x∥) :=
+⟨∥c∥ + 1, @tendsto.eventually ι α f _ _ (λ k, ∥k∥ ≤ ∥c∥ + 1) h (filter.eventually_iff_exists_mem.mpr
+  ⟨metric.closed_ball c 1, metric.closed_ball_mem_nhds c zero_lt_one,
+    λ y hy, norm_le_norm_add_const_of_dist_le hy⟩)⟩
+
 lemma tendsto_zero_iff_norm_tendsto_zero {f : γ → β} {a : filter γ} :
   tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥f e∥) a (𝓝 0) :=
 by { rw [tendsto_iff_norm_tendsto_zero], simp only [sub_zero] }

src/analysis/special_functions/polynomials.lean

@@ -25,7 +25,16 @@ open_locale asymptotics topological_space
 
 namespace polynomial
 
-variables {𝕜 : Type*} [normed_linear_ordered_field 𝕜] [order_topology 𝕜] (P Q : polynomial 𝕜)
+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,
+  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 𝕜]
 
 lemma is_equivalent_at_top_lead :
   (λ x, eval x P) ~[at_top] (λ x, P.leading_coeff * x ^ P.nat_degree) :=
@@ -147,4 +156,17 @@ begin
     exact tendsto_abs_at_bot_at_top.comp (P.div_tendsto_at_bot_of_degree_gt Q hdeg hQ h.le) }
 end
 
+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
+  by_cases hp : P = 0,
+  { simpa [hp] using is_O_zero (λ x, eval x Q) filter.at_top },
+  { have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp,
+    have hPQ : ∀ᶠ (x : 𝕜) in at_top, eval x Q = 0 → eval x P = 0 :=
+      filter.mem_sets_of_superset (polynomial.eventually_no_roots Q hq) (λ x h h', absurd h' h),
+    cases le_iff_lt_or_eq.mp h with h h,
+    { exact is_O_of_div_tendsto_nhds hPQ 0 (div_tendsto_zero_of_degree_lt P Q h) },
+    { exact is_O_of_div_tendsto_nhds hPQ _ (div_tendsto_leading_coeff_div_of_degree_eq P Q h) } }
+end
+
 end polynomial

src/data/polynomial/degree/definitions.lean

@@ -391,6 +391,10 @@ coeff_eq_zero_of_degree_lt (lt_of_lt_of_le h degree_le_nat_degree)
 lemma ne_zero_of_degree_gt {n : with_bot ℕ} (h : n < degree p) : p ≠ 0 :=
 mt degree_eq_bot.2 (ne.symm (ne_of_lt (lt_of_le_of_lt bot_le h)))
 
+lemma ne_zero_of_degree_ge_degree (hpq : p.degree ≤ q.degree) (hp : p ≠ 0) : q ≠ 0 :=
+polynomial.ne_zero_of_degree_gt (lt_of_lt_of_le (bot_lt_iff_ne_bot.mpr
+  (by rwa [ne.def, polynomial.degree_eq_bot])) hpq : q.degree > ⊥)
+
 lemma ne_zero_of_nat_degree_gt {n : ℕ} (h : n < nat_degree p) : p ≠ 0 :=
 λ H, by simpa [H, nat.not_lt_zero] using h
 

src/data/polynomial/ring_division.lean

@@ -324,6 +324,14 @@ begin
   simp only [mem_roots hp, multiset.mem_to_finset, set.mem_set_of_eq, finset.mem_coe]
 end
 
+lemma exists_max_root [linear_order R] (p : polynomial R) (hp : p ≠ 0) :
+  ∃ x₀, ∀ x, p.is_root x → x ≤ x₀ :=
+set.exists_upper_bound_image _ _ $ not_not.mp (mt (eq_zero_of_infinite_is_root p) hp)
+
+lemma exists_min_root [linear_order R] (p : polynomial R) (hp : p ≠ 0) :
+  ∃ x₀, ∀ x, p.is_root x → x₀ ≤ x :=
+set.exists_lower_bound_image _ _ $ not_not.mp (mt (eq_zero_of_infinite_is_root p) hp)
+
 lemma eq_of_infinite_eval_eq {R : Type*} [integral_domain R]
   (p q : polynomial R) (h : set.infinite {x | eval x p = eval x q}) : p = q :=
 begin

src/data/set/finite.lean

@@ -474,6 +474,22 @@ lemma exists_max_image [linear_order β] (s : set α) (f : α → β) (h1 : fini
 | ⟨x, hx⟩ := by simpa only [exists_prop, finite.mem_to_finset]
   using h1.to_finset.exists_max_image f ⟨x, h1.mem_to_finset.2 hx⟩
 
+theorem exists_lower_bound_image [hα : nonempty α] [linear_order β] (s : set α) (f : α → β)
+  (h : s.finite) : ∃ (a : α), ∀ b ∈ s, f a ≤ f b :=
+begin
+  by_cases hs : set.nonempty s,
+  { exact let ⟨x₀, H, hx₀⟩ := set.exists_min_image s f h hs in ⟨x₀, λ x hx, hx₀ x hx⟩ },
+  { exact nonempty.elim hα (λ a, ⟨a, λ x hx, absurd (set.nonempty_of_mem hx) hs⟩) }
+end
+
+theorem exists_upper_bound_image [hα : nonempty α] [linear_order β] (s : set α) (f : α → β)
+  (h : s.finite) : ∃ (a : α), ∀ b ∈ s, f b ≤ f a :=
+begin
+  by_cases hs : set.nonempty s,
+  { exact let ⟨x₀, H, hx₀⟩ := set.exists_max_image s f h hs in ⟨x₀, λ x hx, hx₀ x hx⟩ },
+  { exact nonempty.elim hα (λ a, ⟨a, λ x hx, absurd (set.nonempty_of_mem hx) hs⟩) }
+end
+
 end set
 
 namespace finset