[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖Polynomial.eval x F - Polynomial.eval y F‖ = ‖z‖ * ‖x - y‖
[PROOFSTEP]
simp [hz]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ ≤ 1
[PROOFSTEP]
apply PadicInt.norm_le_one
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ 1 * ‖x - y‖ = ‖x - y‖
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
⊢ Tendsto (fun i => ‖Polynomial.eval (↑ncs i) (↑Polynomial.derivative F)‖) atTop
    (𝓝 ‖Polynomial.eval a (↑Polynomial.derivative F)‖)
[PROOFSTEP]
convert @tendsto_const_nhds ℝ ℕ _ _ _
[GOAL]
case h.e'_3.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
x✝ : ℕ
⊢ ‖Polynomial.eval (↑ncs x✝) (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [ncs_der_val]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
hnorm : Tendsto (fun i => ‖Polynomial.eval (↑ncs i) F‖) atTop (𝓝 0)
⊢ Tendsto (fun e => ‖Polynomial.eval (↑ncs e) F - 0‖) atTop (𝓝 0)
[PROOFSTEP]
simpa using hnorm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
h : ‖Polynomial.eval a (↑Polynomial.derivative F)‖ = 0
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 = 0
[PROOFSTEP]
simp [*, sq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ T_gen p F a = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
simp [T_gen, ← PadicInt.norm_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ T_gen p F a < 1
[PROOFSTEP]
have h := (div_lt_one (deriv_sq_norm_pos hnorm)).2 hnorm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 < 1
⊢ T_gen p F a < 1
[PROOFSTEP]
rw [T_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 < 1
⊢ ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 < 1
[PROOFSTEP]
exact h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ 0
[PROOFSTEP]
simp [T_def, mul_div_cancel' _ (ne_of_gt (deriv_sq_norm_pos hnorm))]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖↑(Polynomial.eval z F)‖ / ‖↑(Polynomial.eval z (↑Polynomial.derivative F))‖ =
    ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [hz.1]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ≤
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
apply hz.2
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖z' - z‖ = ‖z1‖
[PROOFSTEP]
simp only [sub_eq_add_neg, add_assoc, hz', add_add_neg_cancel'_right, norm_neg]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ≤
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
apply hz.2
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
have hdzne : F.derivative.eval z ≠ 0 := mt norm_eq_zero.2 (by rw [hz.1]; apply deriv_norm_ne_zero; assumption)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ¬‖Polynomial.eval z (↑Polynomial.derivative F)‖ = 0
[PROOFSTEP]
rw [hz.1]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ¬‖Polynomial.eval a (↑Polynomial.derivative F)‖ = 0
[PROOFSTEP]
apply deriv_norm_ne_zero
[GOAL]
case hnorm
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
have hdzne' : (↑(F.derivative.eval z) : ℚ_[p]) ≠ 0 := fun h => hdzne (Subtype.ext_iff_val.2 h)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
obtain ⟨q, hq⟩ := F.binomExpansion z (-z1)
[GOAL]
case mk
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
have : ‖(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) : ℚ_[p])‖ ≤ 1 :=
  by
  rw [padicNormE.mul]
  exact mul_le_one (PadicInt.norm_le_one _) (norm_nonneg _) h1
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
⊢ ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
[PROOFSTEP]
rw [padicNormE.mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
⊢ ‖↑(Polynomial.eval z (↑Polynomial.derivative F))‖ *
      ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤
    1
[PROOFSTEP]
exact mul_le_one (PadicInt.norm_le_one _) (norm_nonneg _) h1
[GOAL]
case mk
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
have : F.derivative.eval z * -z1 = -F.eval z := by
  calc
    F.derivative.eval z * -z1 = F.derivative.eval z * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ := by rw [hzeq]
    _ = -(F.derivative.eval z * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) := (mul_neg _ _)
    _ = -⟨F.derivative.eval z * (F.eval z / (F.derivative.eval z : ℤ_[p]) : ℚ_[p]), this⟩ :=
      (Subtype.ext <| by simp only [PadicInt.coe_neg, PadicInt.coe_mul, Subtype.coe_mk])
    _ = -F.eval z := by simp only [mul_div_cancel' _ hdzne', Subtype.coe_eta]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ Polynomial.eval z (↑Polynomial.derivative F) * -z1 = -Polynomial.eval z F
[PROOFSTEP]
calc
  F.derivative.eval z * -z1 = F.derivative.eval z * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ := by rw [hzeq]
  _ = -(F.derivative.eval z * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) := (mul_neg _ _)
  _ = -⟨F.derivative.eval z * (F.eval z / (F.derivative.eval z : ℤ_[p]) : ℚ_[p]), this⟩ :=
    (Subtype.ext <| by simp only [PadicInt.coe_neg, PadicInt.coe_mul, Subtype.coe_mk])
  _ = -F.eval z := by simp only [mul_div_cancel' _ hdzne', Subtype.coe_eta]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ Polynomial.eval z (↑Polynomial.derivative F) * -z1 =
    Polynomial.eval z (↑Polynomial.derivative F) *
      -{ val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
[PROOFSTEP]
rw [hzeq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ ↑(-(Polynomial.eval z (↑Polynomial.derivative F) *
          { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 })) =
    ↑(-{
          val :=
            ↑(Polynomial.eval z (↑Polynomial.derivative F)) *
              (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))),
          property := this })
[PROOFSTEP]
simp only [PadicInt.coe_neg, PadicInt.coe_mul, Subtype.coe_mk]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ -{
        val :=
          ↑(Polynomial.eval z (↑Polynomial.derivative F)) *
            (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))),
        property := this } =
    -Polynomial.eval z F
[PROOFSTEP]
simp only [mul_div_cancel' _ hdzne', Subtype.coe_eta]
[GOAL]
case mk
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this✝ :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
this : Polynomial.eval z (↑Polynomial.derivative F) * -z1 = -Polynomial.eval z F
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
exact ⟨q, by simpa only [sub_eq_add_neg, this, hz', add_right_neg, neg_sq, zero_add] using hq⟩
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this✝ :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
this : Polynomial.eval z (↑Polynomial.derivative F) * -z1 = -Polynomial.eval z F
⊢ Polynomial.eval z' F = q * z1 ^ 2
[PROOFSTEP]
simpa only [sub_eq_add_neg, this, hz', add_right_neg, neg_sq, zero_add] using hq
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval z' F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ (n + 1)
[PROOFSTEP]
calc
  ‖F.eval z'‖ = ‖q‖ * ‖z1‖ ^ 2 := by simp [heq]
  _ ≤ 1 * ‖z1‖ ^ 2 := by gcongr; apply PadicInt.norm_le_one
  _ = ‖F.eval z‖ ^ 2 / ‖F.derivative.eval a‖ ^ 2 := by simp [hzeq, hz.1, div_pow]
  _ ≤ (‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ n) ^ 2 / ‖F.derivative.eval a‖ ^ 2 :=
    by
    gcongr
    exact hz.2
  _ = (‖F.derivative.eval a‖ ^ 2) ^ 2 * (T ^ 2 ^ n) ^ 2 / ‖F.derivative.eval a‖ ^ 2 := by simp only [mul_pow]
  _ = ‖F.derivative.eval a‖ ^ 2 * (T ^ 2 ^ n) ^ 2 := (div_sq_cancel _ _)
  _ = ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ (n + 1) := by
    rw [← pow_mul, pow_succ' 2]
      -- Porting note: unsupported option eqn_compiler.zeta
      -- set_option eqn_compiler.zeta true
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval z' F‖ = ‖q‖ * ‖z1‖ ^ 2
[PROOFSTEP]
simp [heq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖q‖ * ‖z1‖ ^ 2 ≤ 1 * ‖z1‖ ^ 2
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖q‖ ≤ 1
[PROOFSTEP]
apply PadicInt.norm_le_one
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ 1 * ‖z1‖ ^ 2 = ‖Polynomial.eval z F‖ ^ 2 / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
simp [hzeq, hz.1, div_pow]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval z F‖ ^ 2 / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 ≤
    (‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) ^ 2 /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
gcongr
[GOAL]
case h.hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
exact hz.2
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ (‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) ^ 2 /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 =
    (‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2) ^ 2 * (T_gen p F a ^ 2 ^ n) ^ 2 /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
simp only [mul_pow]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * (T_gen p F a ^ 2 ^ n) ^ 2 =
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ (n + 1)
[PROOFSTEP]
rw [← pow_mul, pow_succ' 2]
  -- Porting note: unsupported option eqn_compiler.zeta
  -- set_option eqn_compiler.zeta true
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
z' : ℤ_[p] := z - z1
⊢ ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [hz.1]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
z' : ℤ_[p] := z - z1
hdist :
  ‖Polynomial.eval z' (↑Polynomial.derivative F) - Polynomial.eval z (↑Polynomial.derivative F)‖ <
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖
⊢ ‖Polynomial.eval z' (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [sub_eq_add_neg, ← hz.1, ← norm_neg (F.derivative.eval z)] at hdist 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
z' : ℤ_[p] := z - z1
hdist :
  ‖Polynomial.eval z' (↑Polynomial.derivative F) + -Polynomial.eval z (↑Polynomial.derivative F)‖ <
    ‖-Polynomial.eval z (↑Polynomial.derivative F)‖
⊢ ‖Polynomial.eval z' (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
have := PadicInt.norm_eq_of_norm_add_lt_right hdist
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
z' : ℤ_[p] := z - z1
hdist :
  ‖Polynomial.eval z' (↑Polynomial.derivative F) + -Polynomial.eval z (↑Polynomial.derivative F)‖ <
    ‖-Polynomial.eval z (↑Polynomial.derivative F)‖
this : ‖Polynomial.eval z' (↑Polynomial.derivative F)‖ = ‖-Polynomial.eval z (↑Polynomial.derivative F)‖
⊢ ‖Polynomial.eval z' (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rwa [norm_neg, hz.1] at this 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ ‖newton_seq (n + 1) - newton_seq n‖ =
    ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval (newton_seq n) (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [newton_seq_gen, newton_seq_gen, newton_seq_aux, ih_n]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ ‖↑(let_fun h1 :=
            (_ :
              ‖↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) F) /
                    ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) (↑Polynomial.derivative F))‖ ≤
                1);
          let z1 :=
            {
              val :=
                ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) F) /
                  ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) (↑Polynomial.derivative F)),
              property := h1 };
          let z' := ↑(newton_seq_aux hnorm n) - z1;
          { val := z', property := (_ : ih_gen (n + 1) z') }) -
        ↑(newton_seq_aux hnorm n)‖ =
    ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) F‖ /
      ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [sub_eq_add_neg, add_comm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval (newton_seq n) (↑Polynomial.derivative F)‖ =
    ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [newton_seq_deriv_norm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ T_gen p F a > 0
[PROOFSTEP]
rw [T_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 > 0
[PROOFSTEP]
exact div_pos (norm_pos_iff.2 hnsol) (deriv_sq_norm_pos hnorm)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ 2 ≤ 2 ^ (n + 1)
[PROOFSTEP]
have := pow_le_pow (by norm_num : 1 ≤ 2) (Nat.le_add_left _ _ : 1 ≤ n + 1)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ 1 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ^ 1 ≤ 2 ^ (n + 1)
⊢ 2 ≤ 2 ^ (n + 1)
[PROOFSTEP]
simpa using this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ 1 < 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 1 =
    ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [T_gen, sq, pow_one, norm_div, ← mul_div_assoc, PadicInt.padic_norm_e_of_padicInt, PadicInt.coe_mul, padicNormE.mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * ‖Polynomial.eval a F‖ /
      (‖↑(Polynomial.eval a (↑Polynomial.derivative F))‖ * ‖↑(Polynomial.eval a (↑Polynomial.derivative F))‖) =
    ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
apply mul_div_mul_left
[GOAL]
case hc
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ≠ 0
[PROOFSTEP]
apply deriv_norm_ne_zero
[GOAL]
case hc.hnorm
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ ‖newton_seq (n + 0) - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
simp [T_pow_nonneg, mul_nonneg]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
⊢ 2 ^ n ≤ 2 ^ (n + k)
[PROOFSTEP]
apply pow_le_pow
[GOAL]
case ha
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
⊢ 1 ≤ 2
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
⊢ n ≤ n + k
[PROOFSTEP]
norm_num
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
⊢ n ≤ n + k
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
this : 2 ^ n ≤ 2 ^ (n + k)
⊢ ‖newton_seq (n + (k + 1)) - newton_seq n‖ = ‖newton_seq (n + k + 1) - newton_seq n‖
[PROOFSTEP]
rw [add_assoc]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
this : 2 ^ n ≤ 2 ^ (n + k)
⊢ ‖newton_seq (n + k + 1) - newton_seq n‖ =
    ‖newton_seq (n + k + 1) - newton_seq (n + k) + (newton_seq (n + k) - newton_seq n)‖
[PROOFSTEP]
rw [← sub_add_sub_cancel]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
hnk : n ≤ k
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
have hex : ∃ m, k = n + m := exists_eq_add_of_le hnk
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
let ⟨_, hex'⟩ := hex
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
w✝ : ℕ
hex' : k = n + w✝
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
rw [hex']
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
w✝ : ℕ
hex' : k = n + w✝
⊢ ‖newton_seq (n + w✝) - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
apply newton_seq_dist_aux
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
_h : 0 < 1
⊢ ‖newton_seq 1 - a‖ = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [sub_eq_add_neg, add_assoc, newton_seq_gen, newton_seq_aux, ih_n]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖
[PROOFSTEP]
rw [newton_seq_dist_to_a (k + 1) (succ_pos _)]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
apply newton_seq_succ_dist_weak
[GOAL]
case hnsol
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ Polynomial.eval a F ≠ 0
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
hlt : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖
hne' : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ ≠ ‖newton_seq (k + 1) - a‖
⊢ ‖newton_seq (k + 2) - a‖ = ‖newton_seq (k + 2) - newton_seq (k + 1) + (newton_seq (k + 1) - a)‖
[PROOFSTEP]
rw [← sub_add_sub_cancel]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun n => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)
[PROOFSTEP]
rw [← mul_zero ‖F.derivative.eval a‖]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun n => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop
    (𝓝 (‖Polynomial.eval a (↑Polynomial.derivative F)‖ * 0))
[PROOFSTEP]
exact
  tendsto_const_nhds.mul
    (Tendsto.comp (tendsto_pow_atTop_nhds_0_of_lt_1 (norm_nonneg _) (T_lt_one hnorm))
      (Nat.tendsto_pow_atTop_atTop_of_one_lt (by norm_num)))
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ 1 < 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
have := bound' hnorm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this : Tendsto (fun n => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)
⊢ ∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
simp [Tendsto, nhds] at this 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
⊢ ∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
cases' this (ball 0 ε) (mem_ball_self hε) isOpen_ball with N hN
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ ball 0 ε
⊢ ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
exists N
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ ball 0 ε
⊢ ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
intro n hn
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ ball 0 ε
n : ℕ
hn : n ≥ N
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
simpa [abs_of_nonneg T_nonneg] using hN _ hn
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun n => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)
[PROOFSTEP]
rw [← mul_zero ‖F.derivative.eval a‖, sq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto
    (fun n =>
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * ‖Polynomial.eval a (↑Polynomial.derivative F)‖ *
        T_gen p F a ^ 2 ^ n)
    atTop (𝓝 (‖Polynomial.eval a (↑Polynomial.derivative F)‖ * 0))
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto
    (fun n =>
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ *
        (‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n))
    atTop (𝓝 (‖Polynomial.eval a (↑Polynomial.derivative F)‖ * 0))
[PROOFSTEP]
apply Tendsto.mul
[GOAL]
case hf
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun x => ‖Polynomial.eval a (↑Polynomial.derivative F)‖) atTop
    (𝓝 ‖Polynomial.eval a (↑Polynomial.derivative F)‖)
[PROOFSTEP]
apply tendsto_const_nhds
[GOAL]
case hg
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun x => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ x) atTop (𝓝 0)
[PROOFSTEP]
apply bound'
[GOAL]
case hg.hnorm
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ IsCauSeq norm newton_seq
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖newton_seq j - newton_seq i‖ < ε
[PROOFSTEP]
cases' bound hnorm hε with N hN
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖newton_seq j - newton_seq i‖ < ε
[PROOFSTEP]
exists N
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
⊢ ∀ (j : ℕ), j ≥ N → ‖newton_seq j - newton_seq N‖ < ε
[PROOFSTEP]
intro j hj
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖newton_seq j - newton_seq N‖ < ε
[PROOFSTEP]
apply lt_of_le_of_lt
[GOAL]
case intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖newton_seq j - newton_seq N‖ ≤ ?intro.b
[PROOFSTEP]
apply newton_seq_dist hnorm hj
[GOAL]
case intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ N < ε
[PROOFSTEP]
apply hN
[GOAL]
case intro.a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ N ≥ N
[PROOFSTEP]
exact le_rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖soln - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [soln_dist_to_a, div_lt_iff]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ <
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rwa [sq] at hnorm 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ 0 < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
apply deriv_norm_pos
[GOAL]
case hnorm
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
assumption
[GOAL]
case hnsol
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Polynomial.eval a F ≠ 0
[PROOFSTEP]
exact hnsol
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
⊢ ‖z - soln‖ = ‖z - a + (a - soln)‖
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (soln + h) F
[PROOFSTEP]
simp [hev]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval (soln + h) F = Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
[PROOFSTEP]
rw [hq, eval_soln, zero_add]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2 =
    (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h
[PROOFSTEP]
rw [sq, right_distrib, mul_assoc]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
⊢ Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
[PROOFSTEP]
simpa using eq_neg_of_add_eq_zero_left this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖Polynomial.eval soln (↑Polynomial.derivative F)‖ = ‖-q * h‖
[PROOFSTEP]
rw [this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖-q * h‖ ≤ 1 * ‖h‖
[PROOFSTEP]
rw [PadicInt.norm_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖-q‖ * ‖h‖ ≤ 1 * ‖h‖
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (norm_nonneg _)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ 1 * ‖h‖ = ‖z - soln‖
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖z - soln‖ < ‖Polynomial.eval soln (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [soln_deriv_norm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
apply soln_dist
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
this : h = 0
⊢ z - soln = 0
[PROOFSTEP]
rw [← this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (a + (z' - a)) F
[PROOFSTEP]
rw [add_comm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (z' - a + a) F
[PROOFSTEP]
simp [hz']
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval (a + h) F = Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
[PROOFSTEP]
rw [hq, ha, zero_add]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2 =
    (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h
[PROOFSTEP]
rw [sq, right_distrib, mul_assoc]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
⊢ Polynomial.eval a (↑Polynomial.derivative F) = -q * h
[PROOFSTEP]
simpa using eq_neg_of_add_eq_zero_left this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ = ‖q‖ * ‖h‖
[PROOFSTEP]
simp [this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖q‖ * ‖h‖ ≤ 1 * ‖h‖
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖q‖ ≤ 1
[PROOFSTEP]
apply PadicInt.norm_le_one
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ 1 * ‖h‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simpa
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
this : h = 0
⊢ z' - a = 0
[PROOFSTEP]
rw [← this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
ha : Polynomial.eval a F = 0
⊢ ‖a - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [deriv_ne_zero hnorm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
ha : ¬Polynomial.eval a F = 0
⊢ ∃ z,
    Polynomial.eval z F = 0 ∧
      ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ∧
        ‖Polynomial.eval z (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ∧
          ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ → z' = z
[PROOFSTEP]
exact
  ⟨soln_gen hnorm, eval_soln hnorm, soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z =>
    soln_unique hnorm ha z⟩
