ZetaBnd_aux1b

@[blueprint  (title := "ZetaBnd-aux1b")  (statement := /--  For any $N\ge1$ and $s = \sigma + tI \in \C$, $\sigma > 0$,  $$  \left| \int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right|  \le \frac{N^{-\sigma}}{\sigma}.  $$  -/)  (proof := /-- Apply Lemma \ref{ZetaBnd_aux1a} with $a=N$ and $b\to \infty$. -/)  (latexEnv := "lemma")]lemma ZetaBnd_aux1b (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (σpos : 0 < σ) :    ‖∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖    ≤ N ^ (-σ) / σ := by  apply le_trans (by apply norm_integral_le_integral_norm)  apply le_of_tendsto (x := atTop (α := ℝ)) (f := fun (t : ℝ) ↦ ∫ (x : ℝ) in N..t,    ‖(⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ (σ + t * I + 1)‖) ?_ ?_  · apply intervalIntegral_tendsto_integral_Ioi (μ := volume) (l := atTop) (b := id)      (f := fun (x : ℝ) ↦ ‖(⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ (σ + t * I + 1)‖) N ?_ ?_ |>.congr' ?_    · filter_upwards [Filter.mem_atTop ((N : ℝ))]      intro u hu      simp only [id_eq, intervalIntegral.integral_of_le hu, norm_div]      apply setIntegral_congr_fun (by simp)      intro x hx; beta_reduce      iterate 2 (rw [norm_cpow_eq_rpow_re_of_pos (by linarith [hx.1])])      simp    · apply IntegrableOn.integrable ?_ |>.norm      convert! integrableOn_of_Zeta0_fun (s := σ + t * I) Npos (by simp [σpos]) using 1      simp_rw [div_eq_mul_inv, cpow_neg]    · exact fun ⦃_⦄ a ↦ a  · filter_upwards [mem_atTop (N + 1 : ℝ)] with t ht    have : (N ^ (-σ) - t ^ (-σ)) / σ ≤ N ^ (-σ) / σ :=      div_le_div_iff_of_pos_right σpos |>.mpr (by simp [Real.rpow_nonneg (by linarith)])    apply le_trans ?_ this    convert! ZetaBnd_aux1a (a := N) (b := t) (by positivity) (by linarith) ?_ <;> simp [σpos]