convert ZetaBnd_aux1a (a := N) (b := t) (by positivity) (by linarith) ?_ <;> simp [σpos]
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ (↑N ^ (-σ) - t ^ (-σ)) / σ
no goals