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
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
f : ℝ → ℂ := fun x => ↑⌊x⌋ + 1 / 2 - ↑x
F : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * f x
F' : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * -↑x.log * f x
ε : ℝ := s.re / 2
ε_pos : 0 < ε
bound : ℝ → ℝ := fun x => |x ^ (-s.re / 2 - 1)| * |x.log|
μ : Measure ℝ := volume.restrict (Ioi ↑N)
⊢ 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) * -↑x.log) s
N : ℕ
Npos : 0 < N
s : ℂ
hs : 0 < s.re
f : ℝ → ℂ := fun x => ↑⌊x⌋ + 1 / 2 - ↑x
F : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * f x
F' : ℂ → ℝ → ℂ := fun s x => ↑x ^ (-s - 1) * -↑x.log * f x
ε : ℝ := s.re / 2
ε_pos : 0 < ε
bound : ℝ → ℝ := fun x => |x ^ (-s.re / 2 - 1)| * |x.log|
μ : Measure ℝ := volume.restrict (Ioi ↑N)
hF_meas : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) μ
⊢ 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) * -↑x.log) s