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 < ε
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 < ε
have := bound' 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
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 < ε
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 < ε
simp [Tendsto, nhds] at this
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 < ε
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 < ε
intro ε hε
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 < ε
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 < ε
cases' this (ball 0 ε) (mem_ball_self hε) isOpen_ball with N hN
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 < ε
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 < ε
exists N
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 < ε
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 < ε
intro n hn
no goals
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 < ε
simpa [abs_of_nonneg T_nonneg] using hN _ hn