positivity
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
hN : ¬N = 1
⊢ 0 < ↑N
no goals