ZetaSum_aux2

@[blueprint  (title := "ZetaSum-aux2")  (statement := /--  Let $N$ be a natural number and $s\in \C$, $\Re(s)>1$.  Then  \[  \sum_{N < n} \frac{1}{n^s} =  \frac{- N^{1-s}}{1-s} + \frac{-N^{-s}}{2}    + s \int_N^\infty \frac{\lfloor x\rfloor + 1/2 - x}{x^{s+1}} \, dx.  \]  -/)  (proof := /-- Apply Lemma \ref{ZetaSum_aux1} with $a=N$ and $b\to \infty$. -/)  (latexEnv := "lemma")]lemma ZetaSum_aux2 {N : ℕ} (N_pos : 0 < N) {s : ℂ} (s_re_gt : 1 < s.re) :    ∑' (n : ℕ), 1 / (n + N + 1 : ℂ) ^ s =    (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2      + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)) := by  have s_ne_zero : s ≠ 0 := fun hs ↦ by linarith [zero_re ▸ hs ▸ s_re_gt]  have s_ne_one : s ≠ 1 := fun hs ↦ (lt_self_iff_false _).mp <| one_re ▸ hs ▸ s_re_gt  apply tendsto_nhds_unique (X := ℂ) (Y := ℕ) (l := atTop)    (f := fun k ↦ ((k : ℂ) ^ (1 - s) - (N : ℂ) ^ (1 - s)) / (1 - s) +      1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s)      + s * ∫ (x : ℝ) in (N : ℝ)..k, (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)))    (b := (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2      + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)))  · apply Filter.Tendsto.congr'      (f₁ := fun (k : ℕ) ↦ ∑ n ∈ Finset.Ioc N k, 1 / (n : ℂ) ^ s) (l₁ := atTop)    · apply Filter.eventually_atTop.mpr      use N + 1      intro k hk      exact ZetaSum_aux1 (a := N) (b := k) s_ne_one s_ne_zero ⟨N_pos, hk⟩    · exact ZetaSum_aux3 s_re_gt  · apply (Tendsto.sub ?_ ?_).add (Tendsto.const_mul _ ?_)    · rw [(by ring : -↑N ^ (1 - s) / (1 - s) = (0 - ↑N ^ (1 - s)) / (1 - s) + 0)]      apply cpow_tendsto s_re_gt |>.sub_const _ |>.div_const _ |>.add      simp_rw [mul_comm_div, one_mul, one_div, (by congr; ring : 𝓝 (0 : ℂ) = 𝓝 ((0 : ℂ) / 2))]      apply Tendsto.div_const <| cpow_inv_tendsto (by positivity)    · simp_rw [mul_comm_div, one_mul, one_div, cpow_neg]; exact tendsto_const_nhds    · exact MeasureTheory.intervalIntegral_tendsto_integral_Ioi (a := N)        (b := (fun (n : ℕ) ↦ (n : ℝ)))        (integrableOn_of_Zeta0_fun N_pos <| by positivity) tendsto_natCast_atTop_atTop