ZetaBnd_aux1p

@[blueprint  (title := "ZetaBnd-aux1p")  (statement := /--  For any $N\ge1$ and $s = \sigma + tI \in \C$, $\sigma=\in(0,2], 2 < |t|$,  $$  \left| s\int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx \right|  \ll |t| \frac{N^{-\sigma}}{\sigma}.  $$  -/)  (proof := /-- Apply Lemma \ref{ZetaBnd_aux1b} and estimate $|s|\ll |t|$. -/)  (latexEnv := "lemma")]lemma ZetaBnd_aux1p (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (hσ : σ ∈ Ioc 0 2) :    (fun (t : ℝ) ↦      ‖(σ + t * I) * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖)    =O[Filter.principal {t | 2 ≤ |t|}] fun t ↦ |t| * N ^ (-σ) / σ := by  rw [Asymptotics.IsBigO_def]  use 2  rw [Asymptotics.isBigOWith_principal]  intro t ht  simp only [mem_setOf_eq] at ht  rw [norm_norm, norm_mul, mul_div_assoc, norm_mul]  have : 2 * (‖|t|‖ * ‖↑N ^ (-σ) / σ‖) = (2 * |t|) * ((N : ℝ) ^ (-σ) / σ) := by    simp only [Real.norm_eq_abs, _root_.abs_abs, norm_div]    have : σ ≠ 0 := by linarith [hσ.1]    field_simp    rw [abs_of_pos hσ.1]    have : 0 < (N : ℝ) ^ (-σ) := by      refine Real.rpow_pos_of_pos ?_ _      positivity    rw [abs_of_pos this]    ring  rw [this]  apply mul_le_mul ?_ (ZetaBnd_aux1b N Npos hσ.1) (norm_nonneg _) (by positivity)  refine le_trans (by apply norm_add_le) ?_  simp only [norm_real, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg hσ.1.le, Real.norm_eq_abs]  linarith [hσ.2]