no goals
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)‖
simp [sub_eq_add_neg, add_assoc, newton_seq_gen, newton_seq_aux, ih_n]
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)‖
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‖
rw [newton_seq_dist_to_a (k + 1) (succ_pos _)]
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
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)‖
apply newton_seq_succ_dist_weak
no goals
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
assumption
no goals
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)‖
rw [← sub_add_sub_cancel]