theorem zeta_pole_bound_small_height : ∃ (Z : ℝ), 0 < Z ∧ ∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → |u| ≤ 3 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z / |u|

On a bounded vertical segment to the right of the pole, the Riemann zeta function is bounded by a constant times the reciprocal of the height.

theorem zeta_pole_plus_log_bound : ∃ (Z : ℝ), 0 < Z ∧ ∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)

Uniformly for 0 < x ≤ 1 away from the real pole, zeta has at most logarithmic growth in the height, with the pole recorded by 1 / |u|.