norm_num
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ 9 ≠ 0
no goals