Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_lt_one (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
⊢ Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
Tactic:
have := Tendsto.mul_const C (tendsto_rpow_atTop_of_base_lt_one x (by linarith) x_lt_one)
State after:
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
this : Tendsto (fun k => x ^ k * C) atTop (𝓝 (0 * C))
⊢ Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)

State before:
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
this : Tendsto (fun k => x ^ k * C) atTop (𝓝 (0 * C))
⊢ Tendsto (fun σ => x ^ σ * C) atTop (𝓝 0)
Tactic:
simpa only [rpow_eq_pow, zero_mul] using this
State after:
no goals

State before:
x : ℝ
xpos : 0 < x
x_lt_one : x < 1
C : ℝ
⊢ -1 < x
Tactic:
linarith
State after:
no goals