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))
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)
rw [← MulZeroClass.mul_zero ‖F.derivative.eval a‖, sq]
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))
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))
simp only [mul_assoc]
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)‖)

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)
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))
apply Tendsto.mul
no goals
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)‖)
apply tendsto_const_nhds
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
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)
apply bound'
no goals
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
assumption