refactor(*): drop topology/instances/complex (#5208)

* drop `topology/instances/complex`, deduce topology from `normed_space` instead;
* generalize continuity of `polynomial.eval` to any `topological_ring`; add versions for `eval₂` and `aeval`;
* replace `polynomial.tendsto_infinity` with `tendsto_abv_at_top`, add versions for `eval₂`, `aeval`, as well as `norm` instead of `abv`.
* generalize `complex.exists_forall_abs_polynomial_eval_le` to any `[normed_ring R] [proper_space R]` such that norm
  is multiplicative, rename to `polynomial.exists_forall_norm_le`.

src/analysis/calculus/deriv.lean

@@ -1512,18 +1512,6 @@ begin
   exact p.deriv
 end
 
-protected lemma continuous : continuous (λx, p.eval x) :=
-p.differentiable.continuous
-
-protected lemma continuous_on : continuous_on (λx, p.eval x) s :=
-p.continuous.continuous_on
-
-protected lemma continuous_at : continuous_at (λx, p.eval x) x :=
-p.continuous.continuous_at
-
-protected lemma continuous_within_at : continuous_within_at (λx, p.eval x) s x :=
-p.continuous_at.continuous_within_at
-
 protected lemma has_fderiv_at (x : 𝕜) :
   has_fderiv_at (λx, p.eval x) (smul_right 1 (p.derivative.eval x) : 𝕜 →L[𝕜] 𝕜) x :=
 by simpa [has_deriv_at_iff_has_fderiv_at] using p.has_deriv_at x

src/analysis/calculus/specific_functions.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 import analysis.calculus.extend_deriv
 import analysis.calculus.iterated_deriv
 import analysis.special_functions.exp_log
+import topology.algebra.polynomial
 
 /-!
 # Smoothness of specific functions

src/analysis/complex/basic.lean

@@ -33,6 +33,14 @@ noncomputable theory
 
 namespace complex
 
+instance : has_norm ℂ := ⟨abs⟩
+
+instance : normed_group ℂ :=
+normed_group.of_core ℂ
+{ norm_eq_zero_iff := λ z, abs_eq_zero,
+  triangle := abs_add,
+  norm_neg := abs_neg }
+
 instance : normed_field ℂ :=
 { norm := abs,
   dist_eq := λ _ _, rfl,
@@ -48,6 +56,8 @@ instance normed_algebra_over_reals : normed_algebra ℝ ℂ :=
 
 @[simp] lemma norm_eq_abs (z : ℂ) : ∥z∥ = abs z := rfl
 
+lemma dist_eq (z w : ℂ) : dist z w = abs (z - w) := rfl
+
 @[simp] lemma norm_real (r : ℝ) : ∥(r : ℂ)∥ = ∥r∥ := abs_of_real _
 
 @[simp] lemma norm_rat (r : ℚ) : ∥(r : ℂ)∥ = _root_.abs (r : ℝ) :=
@@ -63,19 +73,13 @@ by rw [norm_real, real.norm_eq_abs]
 lemma norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ∥(n : ℂ)∥ = n :=
 by rw [norm_int, _root_.abs_of_nonneg]; exact int.cast_nonneg.2 hn
 
-/-- Over the complex numbers, any finite-dimensional spaces is proper (and therefore complete).
-We can register this as an instance, as it will not cause problems in instance resolution since
-the properness of `ℂ` is already known and there is no metavariable. -/
-instance finite_dimensional.proper
-  (E : Type) [normed_group E] [normed_space ℂ E] [finite_dimensional ℂ E] : proper_space E :=
-finite_dimensional.proper ℂ E
-attribute [instance, priority 900] complex.finite_dimensional.proper
-
 /-- A complex normed vector space is also a real normed vector space. -/
 @[priority 900]
 instance normed_space.restrict_scalars_real (E : Type*) [normed_group E] [normed_space ℂ E] :
   normed_space ℝ E := normed_space.restrict_scalars ℝ ℂ E
 
+open continuous_linear_map
+
 /-- The space of continuous linear maps over `ℝ`, from a real vector space to a complex vector
 space, is a normed vector space over `ℂ`. -/
 instance continuous_linear_map.real_smul_complex (E : Type*) [normed_group E] [normed_space ℝ E]
@@ -84,12 +88,7 @@ instance continuous_linear_map.real_smul_complex (E : Type*) [normed_group E] [n
 continuous_linear_map.normed_space_extend_scalars
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def continuous_linear_map.re : ℂ →L[ℝ] ℝ :=
-linear_map.re.mk_continuous 1 $ λx, begin
-  change _root_.abs (x.re) ≤ 1 * abs x,
-  rw one_mul,
-  exact abs_re_le_abs x
-end
+def continuous_linear_map.re : ℂ →L[ℝ] ℝ := linear_map.re.to_continuous_linear_map
 
 @[simp] lemma continuous_linear_map.re_coe :
   (coe (continuous_linear_map.re) : ℂ →ₗ[ℝ] ℝ) = linear_map.re := rfl
@@ -99,19 +98,12 @@ end
 
 @[simp] lemma continuous_linear_map.re_norm :
   ∥continuous_linear_map.re∥ = 1 :=
-begin
-  apply le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _),
-  calc 1 = ∥continuous_linear_map.re (1 : ℂ)∥ : by simp
-    ... ≤ ∥continuous_linear_map.re∥ : by { apply continuous_linear_map.unit_le_op_norm, simp }
-end
+le_antisymm (op_norm_le_bound _ zero_le_one $ λ z, by simp [real.norm_eq_abs, abs_re_le_abs]) $
+calc 1 = ∥continuous_linear_map.re 1∥ : by simp
+   ... ≤ ∥continuous_linear_map.re∥ : unit_le_op_norm _ _ (by simp)
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
-def continuous_linear_map.im : ℂ →L[ℝ] ℝ :=
-linear_map.im.mk_continuous 1 $ λx, begin
-  change _root_.abs (x.im) ≤ 1 * abs x,
-  rw one_mul,
-  exact complex.abs_im_le_abs x
-end
+def continuous_linear_map.im : ℂ →L[ℝ] ℝ := linear_map.im.to_continuous_linear_map
 
 @[simp] lemma continuous_linear_map.im_coe :
   (coe (continuous_linear_map.im) : ℂ →ₗ[ℝ] ℝ) = linear_map.im := rfl
@@ -121,16 +113,12 @@ end
 
 @[simp] lemma continuous_linear_map.im_norm :
   ∥continuous_linear_map.im∥ = 1 :=
-begin
-  apply le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _),
-  calc 1 = ∥continuous_linear_map.im (I : ℂ)∥ : by simp
-    ... ≤ ∥continuous_linear_map.im∥ :
-      by { apply continuous_linear_map.unit_le_op_norm, rw ← abs_I, exact le_refl _ }
-end
+le_antisymm (op_norm_le_bound _ zero_le_one $ λ z, by simp [real.norm_eq_abs, abs_im_le_abs]) $
+calc 1 = ∥continuous_linear_map.im I∥ : by simp
+   ... ≤ ∥continuous_linear_map.im∥ : unit_le_op_norm _ _ (by simp)
 
 /-- Continuous linear map version of the canonical embedding of `ℝ` in `ℂ`. -/
-def continuous_linear_map.of_real : ℝ →L[ℝ] ℂ :=
-linear_map.of_real.mk_continuous 1 $ λx, by simp
+def continuous_linear_map.of_real : ℝ →L[ℝ] ℂ := linear_map.of_real.to_continuous_linear_map
 
 @[simp] lemma continuous_linear_map.of_real_coe :
   (coe (continuous_linear_map.of_real) : ℝ →ₗ[ℝ] ℂ) = linear_map.of_real := rfl
@@ -140,12 +128,9 @@ linear_map.of_real.mk_continuous 1 $ λx, by simp
 
 @[simp] lemma continuous_linear_map.of_real_norm :
   ∥continuous_linear_map.of_real∥ = 1 :=
-begin
-  apply le_antisymm (linear_map.mk_continuous_norm_le _ zero_le_one _),
-  calc 1 = ∥continuous_linear_map.of_real (1 : ℝ)∥ : by simp
-    ... ≤ ∥continuous_linear_map.of_real∥ :
-      by { apply continuous_linear_map.unit_le_op_norm, simp }
-end
+le_antisymm (op_norm_le_bound _ zero_le_one $ λ z, by simp) $
+calc 1 = ∥continuous_linear_map.of_real 1∥ : by simp
+   ... ≤ ∥continuous_linear_map.of_real∥ : unit_le_op_norm _ _ (by simp)
 
 lemma continuous_linear_map.of_real_isometry :
   isometry continuous_linear_map.of_real :=

src/analysis/complex/polynomial.lean

@@ -13,26 +13,16 @@ This file proves that every nonconstant complex polynomial has a root.
 -/
 
 open complex polynomial metric filter is_absolute_value set
+open_locale classical
 
 namespace complex
 
-lemma exists_forall_abs_polynomial_eval_le (p : polynomial ℂ) :
-  ∃ x, ∀ y, (p.eval x).abs ≤ (p.eval y).abs :=
-if hp0 : 0 < degree p
-then let ⟨r, hr0, hr⟩ := polynomial.tendsto_infinity complex.abs hp0 ((p.eval 0).abs) in
-  let ⟨x, hx₁, hx₂⟩ := (proper_space.compact_ball (0:ℂ) r).exists_forall_le
-    ⟨0, by simp [le_of_lt hr0]⟩
-    (continuous_abs.comp p.continuous_eval).continuous_on in
-  ⟨x, λ y, if hy : y.abs ≤ r then hx₂ y $ by simpa [complex.dist_eq] using hy
-    else le_trans (hx₂ _ (by simp [le_of_lt hr0])) (le_of_lt (hr y (lt_of_not_ge hy)))⟩
-else ⟨p.coeff 0, by rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]; simp⟩
-
 /- The following proof uses the method given at
   <https://ncatlab.org/nlab/show/fundamental+theorem+of+algebra#classical_fta_via_advanced_calculus> -/
 /-- The fundamental theorem of algebra. Every non constant complex polynomial
   has a root -/
 lemma exists_root {f : polynomial ℂ} (hf : 0 < degree f) : ∃ z : ℂ, is_root f z :=
-let ⟨z₀, hz₀⟩ := exists_forall_abs_polynomial_eval_le f in
+let ⟨z₀, hz₀⟩ := f.exists_forall_norm_le in
 exists.intro z₀ $ classical.by_contradiction $ λ hf0,
 have hfX : f - C (f.eval z₀) ≠ 0,
   from mt sub_eq_zero.1 (λ h, not_le_of_gt hf (h.symm ▸ degree_C_le)),
@@ -42,16 +32,15 @@ have hg0 : g.eval z₀ ≠ 0, from eval_div_by_monic_pow_root_multiplicity_ne_ze
 have hg : g * (X - C z₀) ^ n = f - C (f.eval z₀),
   from div_by_monic_mul_pow_root_multiplicity_eq _ _,
 have hn0 : 0 < n, from nat.pos_of_ne_zero $ λ hn0, by simpa [g, hn0] using hg0,
-let ⟨δ', hδ'₁, hδ'₂⟩ := continuous_iff.1 (polynomial.continuous_eval g) z₀
+let ⟨δ', hδ'₁, hδ'₂⟩ := continuous_iff.1 (polynomial.continuous g) z₀
   ((g.eval z₀).abs) (complex.abs_pos.2 hg0) in
 let δ := min (min (δ' / 2) 1) (((f.eval z₀).abs / (g.eval z₀).abs) / 2) in
 have hf0' : 0 < (f.eval z₀).abs, from complex.abs_pos.2 hf0,
 have hfg0 : 0 < abs (eval z₀ f) * (abs (eval z₀ g))⁻¹, from div_pos hf0' (complex.abs_pos.2 hg0),
 have hδ0 : 0 < δ, from lt_min (lt_min (half_pos hδ'₁) (by norm_num)) (half_pos hfg0),
 have hδ : ∀ z : ℂ, abs (z - z₀) = δ → abs (g.eval z - g.eval z₀) < (g.eval z₀).abs,
   from λ z hz, hδ'₂ z (by rw [complex.dist_eq, hz];
-    exact lt_of_le_of_lt (le_trans (min_le_left _ _) (min_le_left _ _))
-      (half_lt_self hδ'₁)),
+    exact ((min_le_left _ _).trans (min_le_left _ _)).trans_lt (half_lt_self hδ'₁)),
 have hδ1 : δ ≤ 1, from le_trans (min_le_left _ _) (min_le_right _ _),
 let F : polynomial ℂ := C (f.eval z₀) + C (g.eval z₀) * (X - C z₀) ^ n in
 let z' := (-f.eval z₀ * (g.eval z₀).abs * δ ^ n /

src/analysis/normed_space/basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl
 -/
 import topology.instances.nnreal
-import topology.instances.complex
 import topology.algebra.module
 import topology.metric_space.antilipschitz
 

src/data/padics/hensel.lean

@@ -49,7 +49,7 @@ open filter metric
 private lemma comp_tendsto_lim {p : ℕ} [fact p.prime] {F : polynomial ℤ_[p]}
   (ncs : cau_seq ℤ_[p] norm) :
   tendsto (λ i, F.eval (ncs i)) at_top (𝓝 (F.eval ncs.lim)) :=
-(F.continuous_eval.tendsto _).comp ncs.tendsto_limit
+F.continuous_at.tendsto.comp ncs.tendsto_limit
 
 section
 parameters {p : ℕ} [fact p.prime] {ncs : cau_seq ℤ_[p] norm} {F : polynomial ℤ_[p]} {a : ℤ_[p]}

src/measure_theory/borel_space.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury Kudryashov
 -/
 import measure_theory.measure_space
+import analysis.complex.basic
 import analysis.normed_space.finite_dimension
 import topology.G_delta
 

src/topology/algebra/polynomial.lean

@@ -2,47 +2,131 @@
 Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Robert Y. Lewis
-
-Analytic facts about polynomials.
 -/
-import topology.algebra.ring
+import data.polynomial.algebra_map
 import data.polynomial.div
-import data.real.cau_seq
-
-open polynomial is_absolute_value
-
-lemma polynomial.tendsto_infinity {α β : Type*} [comm_ring α] [linear_ordered_field β]
-  (abv : α → β) [is_absolute_value abv] {p : polynomial α} (h : 0 < degree p) :
-  ∀ x : β, ∃ r > 0, ∀ z : α, r < abv z → x < abv (p.eval z) :=
-degree_pos_induction_on p h
-  (λ a ha x, ⟨max (x / abv a) 1, (lt_max_iff.2 (or.inr zero_lt_one)), λ z hz,
-    by simp [max_lt_iff, div_lt_iff' ((abv_pos abv).2 ha), abv_mul abv] at *; tauto⟩)
-  (λ p hp ih x, let ⟨r, hr0, hr⟩ := ih x in
-    ⟨max r 1, lt_max_iff.2 (or.inr zero_lt_one), λ z hz, by rw [eval_mul, eval_X, abv_mul abv];
-        calc x < abv (p.eval z) : hr _ (max_lt_iff.1 hz).1
-        ... ≤ abv (eval z p) * abv z : le_mul_of_one_le_right
-          (abv_nonneg _ _) (max_le_iff.1 (le_of_lt hz)).2⟩)
-  (λ p a hp ih x, let ⟨r, hr0, hr⟩ := ih (x + abv a) in
-    ⟨r, hr0, λ z hz, by rw [eval_add, eval_C, ← sub_neg_eq_add];
-      exact lt_of_lt_of_le (lt_sub_iff_add_lt.2
-        (by rw abv_neg abv; exact (hr z hz)))
-        (le_trans (le_abs_self _) (abs_abv_sub_le_abv_sub _ _ _))⟩)
+import topology.metric_space.cau_seq_filter
+
+/-!
+# Polynomials and limits
+
+In this file we prove the following lemmas.
+
+* `polynomial.continuous_eval₂: `polynomial.eval₂` defines a continuous function.
+* `polynomial.continuous_aeval: `polynomial.aeval` defines a continuous function;
+  we also prove convenience lemmas `polynomial.continuous_at_aeval`,
+  `polynomial.continuous_within_at_aeval`, `polynomial.continuous_on_aeval`.
+* `polynomial.continuous`:  `polynomial.eval` defines a continuous functions;
+  we also prove convenience lemmas `polynomial.continuous_at`, `polynomial.continuous_within_at`,
+  `polynomial.continuous_on`.
+* `polynomial.tendsto_norm_at_top`: `λ x, ∥polynomial.eval (z x) p∥` tends to infinity provided that
+  `λ x, ∥z x∥` tends to infinity and `0 < degree p`;
+* `polynomial.tendsto_abv_eval₂_at_top`, `polynomial.tendsto_abv_at_top`,
+  `polynomial.tendsto_abv_aeval_at_top`: a few versions of the previous statement for
+  `is_absolute_value abv` instead of norm.
+
+## Tags
+
+polynomial, continuity
+-/
+
+open is_absolute_value filter
+
+namespace polynomial
+
+section topological_semiring
+
+variables {R S : Type*} [semiring R] [topological_space R] [topological_semiring R]
+  (p : polynomial R)
 
 @[continuity]
-lemma polynomial.continuous_eval {α} [comm_semiring α] [topological_space α]
-  [topological_semiring α] (p : polynomial α) : continuous (λ x, p.eval x) :=
+protected lemma continuous_eval₂ [semiring S] (p : polynomial S) (f : S →+* R) :
+  continuous (λ x, p.eval₂ f x) :=
 begin
-  apply p.induction,
-  { convert continuous_const,
-    ext, exact eval_zero, },
-  { intros a b f haf hb hcts,
-    simp only [polynomial.eval_add],
-    refine continuous.add _ hcts,
-    have : ∀ x, finsupp.sum (finsupp.single a b) (λ (e : ℕ) (a : α), a * x ^ e) = b * x ^a,
-      from λ x, finsupp.sum_single_index (by simp),
-    convert continuous.mul _ _,
-    { ext, dsimp only [eval_eq_sum], apply this },
-    { apply_instance },
-    { apply continuous_const },
-    { apply continuous_pow }}
+  dsimp only [eval₂_eq_sum, finsupp.sum],
+  exact continuous_finset_sum _ (λ c hc, continuous_const.mul (continuous_pow _))
 end
+
+@[continuity]
+protected lemma continuous : continuous (λ x, p.eval x) :=
+p.continuous_eval₂ _
+
+protected lemma continuous_at {a : R} : continuous_at (λ x, p.eval x) a :=
+p.continuous.continuous_at
+
+protected lemma continuous_within_at {s a} : continuous_within_at (λ x, p.eval x) s a :=
+p.continuous.continuous_within_at
+
+protected lemma continuous_on {s} : continuous_on (λ x, p.eval x) s :=
+p.continuous.continuous_on
+
+end topological_semiring
+
+section topological_algebra
+
+variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A]
+  [topological_space A] [topological_semiring A]
+  (p : polynomial R)
+
+
+@[continuity]
+protected lemma continuous_aeval : continuous (λ x : A, aeval x p) :=
+p.continuous_eval₂ _
+
+protected lemma continuous_at_aeval {a : A} : continuous_at (λ x : A, aeval x p) a :=
+p.continuous_aeval.continuous_at
+
+protected lemma continuous_within_at_aeval {s a} : continuous_within_at (λ x : A, aeval x p) s a :=
+p.continuous_aeval.continuous_within_at
+
+protected lemma continuous_on_aeval {s} : continuous_on (λ x : A, aeval x p) s :=
+p.continuous_aeval.continuous_on
+
+end topological_algebra
+
+lemma tendsto_abv_eval₂_at_top {R S k α : Type*} [semiring R] [ring S] [linear_ordered_field k]
+  (f : R →+* S) (abv : S → k) [is_absolute_value abv] (p : polynomial R) (hd : 0 < degree p)
+  (hf : f p.leading_coeff ≠ 0) {l : filter α} {z : α → S} (hz : tendsto (abv ∘ z) l at_top) :
+  tendsto (λ x, abv (p.eval₂ f (z x))) l at_top :=
+begin
+  revert hf, refine degree_pos_induction_on p hd _ _ _; clear hd p,
+  { rintros c - hc,
+    rw [leading_coeff_mul_X, leading_coeff_C] at hc,
+    simpa [abv_mul abv] using tendsto_at_top_mul_left' ((abv_pos abv).2 hc) hz },
+  { intros p hpd ihp hf,
+    rw [leading_coeff_mul_X] at hf,
+    simpa [abv_mul abv] using tendsto_at_top_mul_at_top (ihp hf) hz },
+  { intros p a hd ihp hf,
+    rw [add_comm, leading_coeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf,
+    refine tendsto_at_top_of_add_const_right (abv (-f a)) _,
+    refine tendsto_at_top_mono (λ _, abv_add abv _ _) _,
+    simpa using ihp hf }
+end
+
+lemma tendsto_abv_at_top {R k α : Type*} [ring R] [linear_ordered_field k]
+  (abv : R → k) [is_absolute_value abv] (p : polynomial R) (h : 0 < degree p)
+  {l : filter α} {z : α → R} (hz : tendsto (abv ∘ z) l at_top) :
+  tendsto (λ x, abv (p.eval (z x))) l at_top :=
+tendsto_abv_eval₂_at_top _ _ _ h (mt leading_coeff_eq_zero.1 $ ne_zero_of_degree_gt h) hz
+
+lemma tendsto_abv_aeval_at_top {R A k α : Type*} [comm_semiring R] [ring A] [algebra R A]
+  [linear_ordered_field k] (abv : A → k) [is_absolute_value abv] (p : polynomial R)
+  (hd : 0 < degree p) (h₀ : algebra_map R A p.leading_coeff ≠ 0)
+  {l : filter α} {z : α → A} (hz : tendsto (abv ∘ z) l at_top) :
+  tendsto (λ x, abv (aeval (z x) p)) l at_top :=
+tendsto_abv_eval₂_at_top _ abv p hd h₀ hz
+
+variables {α R : Type*} [normed_ring R] [is_absolute_value (norm : R → ℝ)]
+
+lemma tendsto_norm_at_top (p : polynomial R) (h : 0 < degree p) {l : filter α} {z : α → R}
+  (hz : tendsto (λ x, ∥z x∥) l at_top) :
+  tendsto (λ x, ∥p.eval (z x)∥) l at_top :=
+p.tendsto_abv_at_top norm h hz
+
+lemma exists_forall_norm_le [proper_space R] (p : polynomial R) :
+  ∃ x, ∀ y, ∥p.eval x∥ ≤ ∥p.eval y∥ :=
+if hp0 : 0 < degree p
+then p.continuous.norm.exists_forall_le $ p.tendsto_norm_at_top hp0 tendsto_norm_cocompact_at_top
+else ⟨p.coeff 0, by rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]; simp⟩
+
+end polynomial