Zeta1AltFormula

@[blueprint "Zeta1AltFormula"  (title := "Zeta1AltFormula")  (statement := /--    We have that    $$\zeta_1(s)=\zeta_0(1,s)$$    where $\zeta_0(1,s)$ comes from Definition \ref{riemannZeta0}.  -/)  (proof := /--    Note that    $$\zeta_0(1,s)=1+\frac{-1}{1-s}+\frac{-1}{2}+s\int_1^\infty\frac{\lfloor x\rfloor+1/2-x}{x^{s+1}}\,dx.$$    With minor simplifications we have    $$\zeta_0(1,s)=1+\frac{1}{s-1}-\frac{1}{2}+\frac{s}{2}\int_1^\infty x^{-s-1}\,dx-s\int_1^\infty\{x\}\,x^{-s-1}\,dx.$$    The first integral evaluates to $1/s$ (when $0<\mathfrak{R}s$), so this term when multiplied by the $s/2$ cancels with the $-1/2$. This exactly gives $\zeta_1$.  -/)]lemma Zeta1AltFormula {s : ℂ} (hs : 0 < s.re) :    ζ₁ s = riemannZeta0 1 s := by  have := Int.self_sub_floor (R := ℝ)  have s_ne_zero : s ≠ 0 := by    intro h; have : s.re = 0 := by simp only [h, zero_re]    linarith  simp only [riemannZeta1, riemannZeta0, Finset.sum_range_succ, Finset.sum_range_zero, div_zero,    CharP.cast_eq_zero, zero_add, cast_one, one_cpow, ne_eq, one_ne_zero, not_false_eq_true,    div_self, Complex.zero_cpow s_ne_zero, zero_add, ← div_neg_eq_neg_div', neg_sub, Int.fract]  rw [sub_eq_add_neg, ← mul_neg, ← MeasureTheory.integral_neg]  nth_rewrite 2 [add_assoc]  rw [add_left_cancel_iff, neg_sub_left, add_comm 1 s]  simp only [← neg_mul, ← Complex.ofReal_neg, neg_sub, div_eq_mul_inv, one_mul, add_sub_right_comm, add_mul, ← Complex.cpow_neg, neg_add, ← sub_eq_add_neg]  rw [MeasureTheory.integral_add, MeasureTheory.integral_const_mul, integral_Ioi_cpow_of_lt _ zero_lt_one]  · push_cast; simp only [inv_neg, sub_add_cancel, one_cpow,      neg_div_neg_eq, one_div, mul_add, ← mul_assoc, mul_right_comm, mul_inv_cancel₀ s_ne_zero]    norm_num  · simp only [neg_re, one_re, sub_re]    linarith  · refine MeasureTheory.Integrable.mono' (integrableOn_Ioi_rpow_of_lt (by linarith) (by linarith)) ?_ ?_ (g := fun u => u ^ ( -s.re - 1 ))    · apply Measurable.aestronglyMeasurable      refine Measurable.mul ?_ (Complex.measurable_ofReal.pow_const _)      exact (Measurable.of_discrete.comp Int.measurable_floor).sub Complex.measurable_ofReal    · filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Ioi] with x hx      norm_num [Complex.norm_cpow_eq_rpow_re_of_pos ( zero_lt_one.trans hx )]      apply mul_le_of_le_one_left (Real.rpow_nonneg (by linarith [hx.out]) _)      norm_cast; rw [← norm_neg, neg_sub, ← Int.fract, Real.norm_of_nonneg (Int.fract_nonneg _)]      exact (Int.fract_lt_one _).le  · refine MeasureTheory.Integrable.mono' (integrableOn_Ioi_rpow_of_lt (by linarith) (by linarith)) ?_ ?_ (g := fun u => u ^ ( -s.re - 1 ))    · apply Measurable.aestronglyMeasurable      exact measurable_const.mul (Complex.measurable_ofReal.pow_const _)    · filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Ioi] with x hx      norm_num [Complex.norm_cpow_eq_rpow_re_of_pos ( zero_lt_one.trans hx )]      exact mul_le_of_le_one_left (Real.rpow_nonneg (by linarith [hx.out]) _) (one_half_lt_one).le