feat(data/padics): use prime typeclass

analysis/polynomial.lean

@@ -0,0 +1,27 @@
+/-
+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 analysis.topology.topological_structures data.polynomial
+
+lemma polynomial.continuous_eval {α} [comm_semiring α] [decidable_eq α] [topological_space α]
+  [topological_semiring α] (p : polynomial α) : continuous (λ x, p.eval x) :=
+begin
+  apply p.induction,
+  { convert continuous_const,
+    ext, show polynomial.eval x 0 = 0, from rfl },
+  { 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, apply this },
+    { apply_instance },
+    { apply continuous_const },
+    { apply continuous_pow }}
+end

data/padics/hensel.lean

@@ -8,13 +8,13 @@ http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf
 -/
 
 import data.padics.padic_integers data.polynomial data.nat.binomial data.real.cau_seq_filter
-       analysis.limits tactic.ring
+       analysis.limits analysis.polynomial tactic.ring
 
 noncomputable theory
 
 local attribute [instance] classical.prop_decidable
 
-lemma padic_polynomial_dist {p : ℕ} {hp : p.prime} (F : polynomial ℤ_[hp]) (x y : ℤ_[hp]) :
+lemma padic_polynomial_dist {p : ℕ} [p.prime] (F : polynomial ℤ_[p]) (x y : ℤ_[p]) :
   ∥F.eval x - F.eval y∥ ≤ ∥x - y∥ :=
 let ⟨z, hz⟩ := F.eval_sub_factor x y in calc
   ∥F.eval x - F.eval y∥ = ∥z∥ * ∥x - y∥ : by simp [hz]
@@ -23,16 +23,16 @@ let ⟨z, hz⟩ := F.eval_sub_factor x y in calc
 
 open filter
 
-private lemma comp_tendsto_lim {p : ℕ} {hp : p.prime} {F : polynomial ℤ_[hp]} (ncs : cau_seq ℤ_[hp] norm) :
-  tendsto (λ i, F.eval (ncs i)) at_top (nhds (F.eval (padic_int.cau_seq_lim ncs))) :=
+private lemma comp_tendsto_lim {p : ℕ} [p.prime] {F : polynomial ℤ_[p]} (ncs : cau_seq ℤ_[p] norm) :
+  tendsto (λ i, F.eval (ncs i)) at_top (nhds (F.eval ncs.lim)) :=
 @tendsto.comp _ _ _ ncs
   (λ k, F.eval k)
   _ _ _
-  (padic_int.tendsto_limit ncs)
+  (tendsto_limit ncs)
   (continuous_iff_tendsto.1 F.continuous_eval _)
 
 section
-parameters {p : ℕ} {hp : p.prime} {ncs : cau_seq ℤ_[hp] norm} {F : polynomial ℤ_[hp]} {a : ℤ_[hp]}
+parameters {p : ℕ} [nat.prime p] {ncs : cau_seq ℤ_[p] norm} {F : polynomial ℤ_[p]} {a : ℤ_[p]}
            (ncs_der_val : ∀ n, ∥F.derivative.eval (ncs n)∥ = ∥F.derivative.eval a∥)
 include ncs_der_val
 
@@ -41,31 +41,31 @@ private lemma ncs_tendsto_const :
 by convert tendsto_const_nhds; ext; rw ncs_der_val
 
 private lemma ncs_tendsto_lim :
-  tendsto (λ i, ∥F.derivative.eval (ncs i)∥) at_top (nhds (∥F.derivative.eval (padic_int.cau_seq_lim ncs)∥)) :=
+  tendsto (λ i, ∥F.derivative.eval (ncs i)∥) at_top (nhds (∥F.derivative.eval ncs.lim∥)) :=
 tendsto.comp (comp_tendsto_lim _) (continuous_iff_tendsto.1 continuous_norm _)
 
-private lemma norm_deriv_eq : ∥F.derivative.eval (padic_int.cau_seq_lim ncs)∥ = ∥F.derivative.eval a∥ :=
+private lemma norm_deriv_eq : ∥F.derivative.eval ncs.lim∥ = ∥F.derivative.eval a∥ :=
 tendsto_nhds_unique at_top_ne_bot ncs_tendsto_lim ncs_tendsto_const
 
 end
 
 section
-parameters {p : ℕ} {hp : p.prime} {ncs : cau_seq ℤ_[hp] norm} {F : polynomial ℤ_[hp]}
+parameters {p : ℕ} [nat.prime p] {ncs : cau_seq ℤ_[p] norm} {F : polynomial ℤ_[p]}
            (hnorm : tendsto (λ i, ∥F.eval (ncs i)∥) at_top (nhds 0))
 include hnorm
 
 private lemma tendsto_zero_of_norm_tendsto_zero : tendsto (λ i, F.eval (ncs i)) at_top (nhds 0) :=
 tendsto_iff_norm_tendsto_zero.2 (by simpa using hnorm)
 
-lemma limit_zero_of_norm_tendsto_zero : F.eval (padic_int.cau_seq_lim ncs) = 0 :=
+lemma limit_zero_of_norm_tendsto_zero : F.eval ncs.lim = 0 :=
 tendsto_nhds_unique at_top_ne_bot (comp_tendsto_lim _) tendsto_zero_of_norm_tendsto_zero
 
 end
 
 section hensel
 open nat
 
-parameters {p : ℕ} {hp : prime p} {F : polynomial ℤ_[hp]} {a : ℤ_[hp]}
+parameters {p : ℕ} [nat.prime p] {F : polynomial ℤ_[p]} {a : ℤ_[p]}
            (hnorm : ∥F.eval a∥ < ∥F.derivative.eval a∥^2) (hnsol : F.eval a ≠ 0)
 include hnorm
 
@@ -101,23 +101,23 @@ private lemma T_pow' (n : ℕ) : T ^ (2 ^ n) < 1 := (T_pow (nat.pow_pos (by norm
 
 private lemma T_pow_nonneg (n : ℕ) : T ^ n ≥ 0 := pow_nonneg (norm_nonneg _) _
 
-private def ih (n : ℕ) (z : ℤ_[hp]) : Prop :=
+private def ih (n : ℕ) (z : ℤ_[p]) : Prop :=
 ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧ ∥F.eval z∥ ≤ ∥F.derivative.eval a∥^2 * T ^ (2^n)
 
 private lemma ih_0 : ih 0 a :=
 ⟨ rfl, by simp [T_def, mul_div_cancel' _ (ne_of_gt (deriv_sq_norm_pos hnorm))] ⟩
 
-private lemma calc_norm_le_one {n : ℕ} {z : ℤ_[hp]} (hz : ih n z) :
-         ∥(↑(F.eval z) : ℚ_[hp]) / ↑(F.derivative.eval z)∥ ≤ 1 :=
-calc ∥(↑(F.eval z) : ℚ_[hp]) / ↑(F.derivative.eval z)∥
-    = ∥(↑(F.eval z) : ℚ_[hp])∥ / ∥(↑(F.derivative.eval z) : ℚ_[hp])∥ : norm_div _ _
+private lemma calc_norm_le_one {n : ℕ} {z : ℤ_[p]} (hz : ih n z) :
+         ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1 :=
+calc ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥
+    = ∥(↑(F.eval z) : ℚ_[p])∥ / ∥(↑(F.derivative.eval z) : ℚ_[p])∥ : norm_div _ _
 ... = ∥F.eval z∥ / ∥F.derivative.eval a∥ : by simp [hz.1]
 ... ≤ ∥F.derivative.eval a∥^2 * T^(2^n) / ∥F.derivative.eval a∥ :
   (div_le_div_right deriv_norm_pos).2 hz.2
 ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel (ne_of_gt deriv_norm_pos) _
 ... ≤ 1 : mul_le_one (padic_norm_z.le_one _) (T_pow_nonneg _) (le_of_lt (T_pow' _))
 
-private lemma calc_deriv_dist {z z' z1 : ℤ_[hp]} (hz' : z' = z - z1)
+private lemma calc_deriv_dist {z z' z1 : ℤ_[p]} (hz' : z' = z - z1)
   (hz1 : ∥z1∥ = ∥F.eval z∥ / ∥F.derivative.eval a∥) {n} (hz : ih n z) :
   ∥F.derivative.eval z' - F.derivative.eval z∥ < ∥F.derivative.eval a∥ :=
 calc
@@ -129,15 +129,15 @@ calc
 ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel deriv_norm_ne_zero _
 ... < ∥F.derivative.eval a∥ : (mul_lt_iff_lt_one_right deriv_norm_pos).2 (T_pow (pow_pos (by norm_num) _))
 
-private def calc_eval_z'  {z z' z1 : ℤ_[hp]} (hz' : z' = z - z1) {n} (hz : ih n z)
-  (h1 : ∥(↑(F.eval z) : ℚ_[hp]) / ↑(F.derivative.eval z)∥ ≤ 1) (hzeq : z1 = ⟨_, h1⟩) :
-  {q : ℤ_[hp] // F.eval z' = q * z1^2} :=
-have hdzne' : (↑(F.derivative.eval z) : ℚ_[hp]) ≠ 0, from
+private def calc_eval_z'  {z z' z1 : ℤ_[p]} (hz' : z' = z - z1) {n} (hz : ih n z)
+  (h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1) (hzeq : z1 = ⟨_, h1⟩) :
+  {q : ℤ_[p] // F.eval z' = q * z1^2} :=
+have hdzne' : (↑(F.derivative.eval z) : ℚ_[p]) ≠ 0, from
   have hdzne : F.derivative.eval z ≠ 0,
     from mt (norm_eq_zero _).2 (by rw hz.1; apply deriv_norm_ne_zero; assumption),
   λ h, hdzne $ subtype.ext.2 h,
 let ⟨q, hq⟩ := F.binom_expansion z (-z1) in
-have ∥(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) : ℚ_[hp])∥ ≤ 1,
+have ∥(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) : ℚ_[p])∥ ≤ 1,
   by {rw padic_norm_e.mul, apply mul_le_one, apply padic_norm_z.le_one, apply norm_nonneg, apply h1},
 have F.derivative.eval z * (-z1) = -F.eval z, from calc
   F.derivative.eval z * (-z1)
@@ -148,8 +148,8 @@ have F.derivative.eval z * (-z1) = -F.eval z, from calc
 have heq : F.eval z' = q * z1^2, by simpa [this, hz'] using hq,
 ⟨q, heq⟩
 
-private def calc_eval_z'_norm {z z' z1 : ℤ_[hp]} {n} (hz : ih n z) {q}
-  (heq : F.eval z' = q * z1^2) (h1 : ∥(↑(F.eval z) : ℚ_[hp]) / ↑(F.derivative.eval z)∥ ≤ 1)
+private def calc_eval_z'_norm {z z' z1 : ℤ_[p]} {n} (hz : ih n z) {q}
+  (heq : F.eval z' = q * z1^2) (h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1)
   (hzeq : z1 = ⟨_, h1⟩) : ∥F.eval z'∥ ≤ ∥F.derivative.eval a∥^2 * T^(2^(n+1)) :=
 calc ∥F.eval z'∥
     = ∥q∥ * ∥z1∥^2 : by simp [heq]
@@ -165,10 +165,10 @@ calc ∥F.eval z'∥
 set_option eqn_compiler.zeta true
 
 -- we need (ih k) in order to construct the value for k+1, otherwise it might not be an integer.
-private def ih_n {n : ℕ} {z : ℤ_[hp]} (hz : ih n z) : {z' : ℤ_[hp] // ih (n+1) z'} :=
-have h1 : ∥(↑(F.eval z) : ℚ_[hp]) / ↑(F.derivative.eval z)∥ ≤ 1, from calc_norm_le_one hz,
-let z1 : ℤ_[hp] := ⟨_, h1⟩,
-    z' : ℤ_[hp] := z - z1 in
+private def ih_n {n : ℕ} {z : ℤ_[p]} (hz : ih n z) : {z' : ℤ_[p] // ih (n+1) z'} :=
+have h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1, from calc_norm_le_one hz,
+let z1 : ℤ_[p] := ⟨_, h1⟩,
+    z' : ℤ_[p] := z - z1 in
 ⟨ z',
   have hdist : ∥F.derivative.eval z' - F.derivative.eval z∥ < ∥F.derivative.eval a∥,
     from calc_deriv_dist rfl (by simp [z1, hz.1]) hz,
@@ -186,11 +186,11 @@ let z1 : ℤ_[hp] := ⟨_, h1⟩,
 set_option eqn_compiler.zeta false
 
 -- why doesn't "noncomputable theory" stick here?
-private noncomputable def newton_seq_aux : Π n : ℕ, {z : ℤ_[hp] // ih n z}
+private noncomputable def newton_seq_aux : Π n : ℕ, {z : ℤ_[p] // ih n z}
 | 0 := ⟨a, ih_0⟩
 | (k+1) := ih_n (newton_seq_aux k).2
 
-private def newton_seq (n : ℕ) : ℤ_[hp] := (newton_seq_aux n).1
+private def newton_seq (n : ℕ) : ℤ_[p] := (newton_seq_aux n).1
 
 private lemma newton_seq_deriv_norm (n : ℕ) :
   ∥F.derivative.eval (newton_seq n)∥ = ∥F.derivative.eval a∥ :=
@@ -295,8 +295,7 @@ begin
   intros ε hε,
   cases this (ball 0 ε) (mem_ball_self hε) (is_open_ball) with N hN,
   existsi N, intros n hn,
-  have := hN _ hn,
-  simpa [normed_field.norm_mul, real.norm_eq_abs, abs_of_nonneg (mtn n)] using this
+  simpa [normed_field.norm_mul, real.norm_eq_abs, abs_of_nonneg (mtn n)] using hN _ hn
 end
 
 private lemma bound'_sq : tendsto (λ n : ℕ, ∥F.derivative.eval a∥^2 * T^(2^n)) at_top (nhds 0) :=
@@ -308,7 +307,7 @@ begin
   { apply bound', assumption }
 end
 
-private theorem newton_seq_is_cauchy : is_cau_seq padic_norm_z newton_seq :=
+private theorem newton_seq_is_cauchy : is_cau_seq norm newton_seq :=
 begin
   intros ε hε,
   cases bound hnorm hnsol hε with N hN,
@@ -319,13 +318,13 @@ begin
   { apply hN, apply le_refl }
 end
 
-private def newton_cau_seq : cau_seq ℤ_[hp] norm := ⟨_, newton_seq_is_cauchy⟩
+private def newton_cau_seq : cau_seq ℤ_[p] norm := ⟨_, newton_seq_is_cauchy⟩
 
-private def soln : ℤ_[hp] := padic_int.cau_seq_lim newton_cau_seq
+private def soln : ℤ_[p] := newton_cau_seq.lim
 
 private lemma soln_spec {ε : ℝ} (hε : ε > 0) :
   ∃ (N : ℕ), ∀ {i : ℕ}, i ≥ N → ∥soln - newton_cau_seq i∥ < ε :=
-padic_int.cau_seq_lim_spec newton_cau_seq _ hε
+cau_seq.lim_spec newton_cau_seq _ hε
 
 private lemma soln_deriv_norm : ∥F.derivative.eval soln∥ = ∥F.derivative.eval a∥ :=
 norm_deriv_eq newton_seq_deriv_norm
@@ -341,7 +340,7 @@ tendsto_cong (tendsto_const_nhds) $
 
 private lemma newton_seq_dist_tendsto' :
   tendsto (λ n, ∥newton_cau_seq n - a∥) at_top (nhds ∥soln - a∥) :=
-tendsto.comp (tendsto_sub (padic_int.tendsto_limit _) tendsto_const_nhds)
+tendsto.comp (tendsto_sub (tendsto_limit _) tendsto_const_nhds)
              (continuous_iff_tendsto.1 continuous_norm _)
 
 private lemma soln_dist_to_a : ∥soln - a∥ = ∥F.eval a∥ / ∥F.derivative.eval a∥ :=
@@ -358,7 +357,7 @@ end
 private lemma eval_soln : F.eval soln = 0 :=
 limit_zero_of_norm_tendsto_zero newton_seq_norm_tendsto_zero
 
-private lemma soln_unique (z : ℤ_[hp]) (hev : F.eval z = 0) (hnlt : ∥z - a∥ < ∥F.derivative.eval a∥) :
+private lemma soln_unique (z : ℤ_[p]) (hev : F.eval z = 0) (hnlt : ∥z - a∥ < ∥F.derivative.eval a∥) :
   z = soln :=
 have soln_dist : ∥z - soln∥ < ∥F.derivative.eval a∥, from calc
   ∥z - soln∥ = ∥(z - a) + (a - soln)∥ : by rw sub_add_sub_cancel
@@ -382,9 +381,9 @@ eq_of_sub_eq_zero (by rw ←this; refl)
 
 end hensel
 
-variables {p : ℕ} {hp : p.prime} {F : polynomial ℤ_[hp]} {a : ℤ_[hp]}
+variables {p : ℕ} [nat.prime p] {F : polynomial ℤ_[p]} {a : ℤ_[p]}
 
-private lemma a_soln_is_unique (ha : F.eval a = 0) (z' : ℤ_[hp]) (hz' : F.eval z' = 0)
+private lemma a_soln_is_unique (ha : F.eval a = 0) (z' : ℤ_[p]) (hz' : F.eval z' = 0)
   (hnormz' : ∥z' - a∥ < ∥F.derivative.eval a∥) : z' = a :=
 let h := z' - a,
     ⟨q, hq⟩ := F.binom_expansion a h in
@@ -409,7 +408,7 @@ private lemma a_is_soln (ha : F.eval a = 0) :
   ∀ z', F.eval z' = 0 → ∥z' - a∥ < ∥F.derivative.eval a∥ → z' = a :=
 ⟨ha, by simp; apply deriv_norm_pos; apply hnorm, rfl, a_soln_is_unique ha⟩
 
-lemma hensels_lemma : ∃ z : ℤ_[hp], F.eval z = 0 ∧ ∥z - a∥ < ∥F.derivative.eval a∥ ∧
+lemma hensels_lemma : ∃ z : ℤ_[p], F.eval z = 0 ∧ ∥z - a∥ < ∥F.derivative.eval a∥ ∧
   ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧
   ∀ z', F.eval z' = 0 → ∥z' - a∥ < ∥F.derivative.eval a∥ → z' = z :=
 if ha : F.eval a = 0 then ⟨a, a_is_soln hnorm ha⟩ else