ZetaBnd_aux1a

@[blueprint  (title := "ZetaBnd-aux1a")  (statement := /--  For any $0 < a < b$ and  $s \in \C$ with $\sigma=\Re(s)>0$,  $$  \int_a^b \left|\frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx\right|  \le \frac{a^{-\sigma}-b^{-\sigma}}{\sigma}.  $$  -/)  (proof := /--  Apply the triangle inequality  $$  \left|\int_a^b \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx\right|  \le \int_a^b \frac{1}{x^{\sigma+1}} \, dx,  $$  and evaluate the integral.  -/)  (latexEnv := "lemma")]lemma ZetaBnd_aux1a {a b : ℝ} (apos : 0 < a) (a_lt_b : a < b) {s : ℂ} (σpos : 0 < s.re) :    ∫ x in a..b, ‖(⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ (s + 1)‖ ≤      (a ^ (-s.re) - b ^ (-s.re)) / s.re := by  calc    _ = ∫ x in a..b, |(⌊x⌋ + 1 / 2 - x)| / x ^ (s+1).re := ZetaSum_aux1_4 apos a_lt_b    _ ≤ ∫ x in a..b, 1 / x ^ (s.re + 1) := ZetaSum_aux1_5 apos a_lt_b σpos    _ = (a ^ (-s.re) - b ^ (-s.re)) / s.re := ?_  refine ZetaSum_aux1_2 (c := s.re) apos a_lt_b ⟨ne_of_gt σpos, ?_⟩  exact fun h ↦ (lt_self_iff_false 0).mp <| ZetaSum_aux1_1 apos a_lt_b h