hasDerivAt_Zeta0Integral

lemma hasDerivAt_Zeta0Integral {N : ℕ} (Npos : 0 < N) {s : ℂ} (hs : s ∈ {s | 0 < s.re}) :  HasDerivAt (fun z ↦ ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-z - 1))    (∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (- s - 1) * (- Real.log x)) s := by  simp only [mem_setOf_eq] at hs  set f : ℝ → ℂ := fun x ↦ (⌊x⌋ : ℂ) + 1 / 2 - x  set F : ℂ → ℝ → ℂ := fun s x ↦ (x : ℂ) ^ (- s - 1) * f x  set F' : ℂ → ℝ → ℂ := fun s x ↦ (x : ℂ) ^ (- s - 1) * (- Real.log x) * f x  set ε := s.re / 2  have ε_pos : 0 < ε := by aesop  set bound : ℝ → ℝ := fun x ↦ |x ^ (- s.re / 2 - 1)| * |Real.log x|  let μ : Measure ℝ := volume.restrict (Ioi (N : ℝ))  have hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ := by    have : {z : ℂ | 0 < z.re} ∈ 𝓝 s := by      rw [mem_nhds_iff]      refine ⟨{z | 0 < z.re}, fun ⦃a⦄ a ↦ a, isOpen_lt continuous_const Complex.continuous_re, hs⟩    filter_upwards [this] with z hz    convert! integrableOn_of_Zeta0_fun Npos hz |>.aestronglyMeasurable using 1    simp only [F, f]; ext x; ring_nf  have hF_int : Integrable (F s) μ := by    convert! integrableOn_of_Zeta0_fun Npos hs |>.integrable using 1    simp only [F, f]; ext x; ring_nf  have hF'_meas : AEStronglyMeasurable (F' s) μ := by    convert! integrableOn_of_Zeta0_fun_log Npos hs |>.aestronglyMeasurable using 1    simp only [F', f]; ext x; ring_nf  have IoiSubIoi1 : (Ioi (N : ℝ)) ⊆ {x | 1 < x} :=      fun x hx ↦ lt_of_le_of_lt (by simp only [Nat.one_le_cast]; omega) <| mem_Ioi.mp hx  have measSetIoi1 : MeasurableSet {x : ℝ | 1 < x} := (isOpen_lt' 1).measurableSet  have h_bound1 :    ∀ᵐ (x : ℝ) ∂volume.restrict {x | 1 < x}, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x := by    filter_upwards [self_mem_ae_restrict measSetIoi1] with x hx    intro z hz    simp only [F', f, bound]    calc _ = ‖(x : ℂ) ^ (-z - 1)‖ * ‖-(Real.log x)‖ * ‖(⌊x⌋ + 1 / 2 - x)‖ := by            simp only [mul_neg, one_div, neg_mul, norm_neg, norm_mul, norm_real, Real.norm_eq_abs,              ← (by simp : (((⌊x⌋ + 2⁻¹ - x) : ℝ) : ℂ) = (⌊x⌋ : ℂ) + 2⁻¹ - ↑x),              Complex.norm_real]         _ = ‖x ^ (-z.re - 1)‖ * ‖-(Real.log x)‖ * ‖(⌊x⌋ + 1 / 2 - x)‖ := ?_         _ = |x ^ (-z.re - 1)| * |(Real.log x)| * |(⌊x⌋ + 1 / 2 - x)| := by simp         _ ≤ _ := ?_    · congr! 2      simp only [Real.norm_eq_abs, norm_cpow_eq_rpow_re_of_pos (by linarith),        sub_re, neg_re, one_re]      apply abs_eq_self.mpr ?_ |>.symm      positivity    · rw [mul_comm, ← mul_assoc]      apply mul_le_mul_of_nonneg_right ?_ <| abs_nonneg _      simp only [Metric.mem_ball, ε, Complex.dist_eq] at hz      apply le_trans (b := 1 * |x ^ (-z.re - 1)|)      · apply mul_le_mul_of_nonneg_right (le_trans (ZetaSum_aux1_3 _) (by norm_num)) <| abs_nonneg _      · simp_rw [one_mul, Real.abs_rpow_of_nonneg (by linarith : 0 ≤ x)]        apply Real.rpow_le_rpow_of_exponent_le <| le_abs.mpr (by left; exact hx.le)        have := abs_le.mp <| le_trans (abs_re_le_norm (z-s)) hz.le        simp only [sub_re, neg_le_sub_iff_le_add, tsub_le_iff_right] at this        linarith [this.1]  have h_bound : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, ‖F' z x‖ ≤ bound x := by    apply ae_restrict_of_ae_restrict_of_subset IoiSubIoi1    exact h_bound1  have bound_integrable : Integrable bound μ := by    simp only [bound]    convert! integrable_log_over_pow (r := -s.re / 2) (by linarith) Npos using 0  have h_diff : ∀ᵐ x ∂μ, ∀ z ∈ Metric.ball s ε, HasDerivAt (fun w ↦ F w x) (F' z x) z := by    simp only [F, F', f]    apply ae_restrict_of_ae_restrict_of_subset IoiSubIoi1    filter_upwards [h_bound1, self_mem_ae_restrict measSetIoi1] with x _ one_lt_x    intro z hz    convert! HasDerivAt.mul_const (c := fun (w : ℂ) ↦ (x : ℂ) ^ (-w-1))      (c' := (x : ℂ) ^ (-z-1) * -Real.log x) (d := (⌊x⌋ : ℝ) + 1 / 2 - x) ?_ using 1    convert! HasDerivAt.comp (h := fun w ↦ -w-1) (h' := -1) (h₂ := fun w ↦ x ^ w)      (h₂' := x ^ (-z-1) * Real.log x) (x := z) ?_ ?_ using 0    · simp only [mul_neg, mul_one]; congr! 2    · convert! HasDerivAt.const_cpow (c := (x : ℂ)) (f := fun w ↦ w) (f' := 1) (x := -z-1)        (hasDerivAt_id _) ?_ using 1      · simp only [mul_one, mul_eq_mul_left_iff, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq]        left        rw [Complex.ofReal_log]        linarith      · right        intro h        simp only [Metric.mem_ball, ε, Complex.dist_eq,          neg_eq_iff_eq_neg.mp <| sub_eq_zero.mp h] at hz        have := (abs_le.mp <| le_trans (abs_re_le_norm (-1-s)) hz.le).1        simp only [sub_re, neg_re, one_re, neg_le_sub_iff_le_add, le_neg_add_iff_add_le] at this        linarith    · apply hasDerivAt_id _ |>.neg |>.sub_const  convert! (hasDerivAt_integral_of_dominated_loc_of_deriv_le (F := F) (F' := F') (x₀ := s)    (s := Metric.ball s ε) (bound := bound) (μ := μ) (Metric.ball_mem_nhds s ε_pos)    hF_meas hF_int hF'_meas h_bound bound_integrable h_diff).2 using 3  · ext a; simp only [one_div, F, f]; ring_nf  · simp only [one_div, mul_neg, neg_mul, neg_inj, F', f]; ring_nf