integrableOn_of_Zeta0_fun_log

lemma integrableOn_of_Zeta0_fun_log {N : ℕ} (Npos : 0 < N) {s : ℂ} (s_re_gt : 0 < s.re) :    IntegrableOn (fun (x : ℝ) ↦ (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)) * (-Real.log x)) (Ioi N)    volume := by  simp_rw [mul_assoc]  obtain ⟨c, hc⟩ := ZetaSum_aux2a  apply Integrable.bdd_mul (c := c) ?_ ?_ ?_  · simp only [neg_add_rev, mul_neg, add_comm, ← sub_eq_add_neg]    apply integrable_norm_iff ?_ |>.mp ?_ |>.neg    · apply ContinuousOn.mul ?_ ?_ |>.aestronglyMeasurable (by simp)      · intro x hx        apply ContinuousWithinAt.cpow ?_ continuous_const.continuousWithinAt ?_        · exact RCLike.continuous_ofReal.continuousWithinAt        · simp only [ofReal_mem_slitPlane]; linarith [mem_Ioi.mp hx]      · apply RCLike.continuous_ofReal.continuousOn.comp ?_ (mapsTo_image _ _)        refine continuous_id.continuousOn.log ?_        intro x hx; simp only [id_eq]; linarith [mem_Ioi.mp hx]    · simp only [norm_mul, norm_real]      have := integrable_log_over_pow (r := -s.re) (by linarith) Npos      apply IntegrableOn.congr_fun this ?_ (by simp)      intro x hx      simp only [mul_eq_mul_right_iff, norm_eq_zero, Real.log_eq_zero]      left      have xpos : 0 < x := by linarith [mem_Ioi.mp hx]      simp [norm_cpow_eq_rpow_re_of_pos xpos, Real.abs_rpow_of_nonneg xpos.le,        abs_eq_self.mpr xpos.le]  · apply Measurable.add ?_ measurable_const |>.sub (by fun_prop) |>.aestronglyMeasurable    exact Measurable.comp (fun _ _ ↦ trivial) Int.measurable_floor  · apply MeasureTheory.ae_of_all    convert hc with _ x; simp only [← Complex.norm_real]; simp