set s := σ + t * I
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ ‖↑n ^ (-(↑σ + ↑t * I))‖ ≤ (↑n)⁻¹ * A.exp
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp