ZetaAppendix.lemma_abadtoabsum

@[blueprint  "lem:abadtoabsum"  (title := "Estimate for a partial sum of $\\zeta(s)$")  (statement := /--Let $b>a>0$, $b\in \mathbb{Z} + \frac{1}{2}$.Then, for all $s\in \mathbb{C}\setminus \{1\}$ with $\sigma = \Re s > 0$,$$\sum_{n\leq a} \frac{1}{n^s} = -\sum_{a < n\leq b} \frac{1}{n^s} + \zeta(s)  + \frac{b^{1-s}}{1-s} + O^*\left(\frac{|s|}{2 \sigma b^\sigma}\right).$$-/)  (proof := /--By Lemma \ref{lem:abadeulmac}, $\sum_{n\leq a} = \sum_{n\leq b} - \sum_{a < n\leq b}$,$\left|\{y\}-\frac{1}{2}\right| \leq \frac{1}{2}$ and$\int_b^\infty \frac{dy}{|y^{s+1}|} = \frac{1}{\sigma b^\sigma}$.-/)  (latexEnv := "lemma")  (discussion := 567)]theorem lemma_abadtoabsum {a b : ℝ} (ha : 0 < a) (hb' : b.IsHalfInteger) (hab : b > a) {s : ℂ}    (hs1 : s ≠ 1) (hsigma : 0 < s.re) :    ∃ E, ∑ n ∈ Icc 1 ⌊a⌋₊, (n : ℂ) ^ (-s) = -∑ n ∈ Ioc ⌊a⌋₊ ⌊b⌋₊,      (n : ℂ) ^ (-s) + riemannZeta s + (b ^ (1 - s) : ℂ) / (1 - s) + E ∧      ‖E‖ ≤ ‖s‖ / (2 * s.re * (b ^ s.re : ℝ)) := by  have hb_pos : 0 < b := ha.trans hab  have hmac := lemma_abadeulmac hb_pos hb' hs1 hsigma  let E := s * ∫ y in Set.Ioi b, (Int.fract y - 1 / 2 : ℂ) * ((y : ℂ) ^ (-(s + 1)))  refine ⟨E, ?_, ?_⟩  · have hfinset : (Icc 1 ⌊b⌋₊ : Finset ℕ) = Finset.Icc 1 ⌊a⌋₊ ∪ Ioc ⌊a⌋₊ ⌊b⌋₊ := by      ext n; simp only [Finset.mem_union, Finset.mem_Icc, Finset.mem_Ioc]      refine ⟨fun ⟨h1, hn⟩ ↦ ?_, fun h ↦ ?_⟩      · by_cases hn' : n ≤ ⌊a⌋₊        · exact Or.inl ⟨h1, hn'⟩        · exact Or.inr ⟨Nat.lt_of_not_le hn', hn⟩      · rcases h with ⟨h1, hn⟩ | ⟨hn1, hn2⟩        · exact ⟨h1, hn.trans <| Nat.floor_mono hab.le⟩        · exact ⟨by omega, hn2⟩    have hdisjoint : Disjoint (Finset.Icc 1 ⌊a⌋₊) (Ioc ⌊a⌋₊ ⌊b⌋₊) :=      disjoint_left.mpr fun x hx₁ hx₂ ↦ by simp only [Finset.mem_Icc] at hx₁; simp only [Finset.mem_Ioc] at hx₂; omega    rw [hfinset, sum_union hdisjoint] at hmac    linear_combination' hmac  · have h_integral_bound : ‖∫ y in Set.Ioi b, (Int.fract y - 1 / 2 : ℂ) * ((y : ℂ) ^ (-(s + 1)))‖ ≤        (1 / 2) * (1 / (s.re * b ^ s.re)) := by      have hstep1 : ‖∫ y in Set.Ioi b, (Int.fract y - 1 / 2 : ℂ) * ((y : ℂ) ^ (-(s + 1)))‖ ≤          ∫ y in Set.Ioi b, ‖(Int.fract y - 1 / 2 : ℂ) * ((y : ℂ) ^ (-(s + 1)))‖ :=        norm_integral_le_integral_norm _      have : ∫ y in Set.Ioi b, ‖(Int.fract y - 1 / 2 : ℂ) * ((y : ℂ) ^ (-(s + 1)))‖ ≤          ∫ y in Set.Ioi b, (1 / 2 : ℝ) * (y : ℝ) ^ (-(s.re + 1)) := by        apply integral_mono_of_nonneg (Filter.Eventually.of_forall fun _ ↦ norm_nonneg _)          ((integrableOn_Ioi_rpow_of_lt (by linarith) hb_pos).const_mul _) _        filter_upwards [ae_restrict_mem measurableSet_Ioi] with y hy        simp only [norm_mul, norm_cpow_eq_rpow_re_of_pos (hb_pos.trans hy), neg_add_rev, add_re,          neg_re, one_re]        apply mul_le_mul_of_nonneg_right _ (rpow_nonneg (hb_pos.trans hy).le _)        rw [norm_sub_rev]        have hfract_bound : ‖(1 / 2 : ℂ) - ↑(Int.fract y)‖ ≤ 1 / 2 := by          have : (1 / 2 : ℂ) - ↑(Int.fract y) = ↑((1 / 2 : ℝ) - (Int.fract y : ℝ)) := by            simp only [ofReal_sub, ofReal_div, ofReal_one, ofReal_ofNat]          rw [this, norm_real, norm_eq_abs, abs_le]          constructor <;> linarith [Int.fract_nonneg y, Int.fract_lt_one y]        exact hfract_bound      have : ∫ y in Set.Ioi b, (1 / 2 : ℝ) * (y : ℝ) ^ (-(s.re + 1)) =          (1 / 2) * (1 / (s.re * b ^ s.re)) := by        rw [integral_const_mul, integral_Ioi_rpow_of_lt (by linarith : -(s.re + 1) < -1) hb_pos]        have : -(s.re + 1) + 1 = -s.re := by ring        have : b ^ (-s.re) = (b ^ s.re)⁻¹ := rpow_neg hb_pos.le s.re        aesop      linarith    calc ‖E‖ = ‖s‖ * ‖∫ y in Set.Ioi b, (Int.fract y - 1 / 2 : ℂ) * ((y : ℂ) ^ (-(s + 1)))‖ := by simp only [E, norm_mul]      _ ≤ ‖s‖ * ((1 / 2) * (1 / (s.re * b ^ s.re))) := mul_le_mul_of_nonneg_left h_integral_bound (norm_nonneg _)      _ = ‖s‖ / (2 * s.re * b ^ s.re) := by ring