ZetaAbelFractKernel.hasDerivAt_integral_param_dominated_Ioi

lemma hasDerivAt_integral_param_dominated_Ioi  (F F' : ℂ → ℝ → ℂ) (s : ℂ) (δ : ℝ) (hδ : 0 < δ)  (hmeas : ∀ᶠ z in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi (1 : ℝ))))  (hFint : Integrable (F s) (volume.restrict (Ioi (1 : ℝ))))  (hF'meas : AEStronglyMeasurable (F' s) (volume.restrict (Ioi (1 : ℝ))))  (bound : ℝ → ℝ) (hbound_int : Integrable bound (volume.restrict (Ioi (1 : ℝ))))  (hbound : ∀ᵐ u ∂(volume.restrict (Ioi (1 : ℝ))), ∀ z ∈ Metric.ball s δ, ‖F' z u‖ ≤ bound u)  (hderiv : ∀ᵐ u ∂(volume.restrict (Ioi (1 : ℝ))), ∀ z ∈ Metric.ball s δ,    HasDerivAt (fun w => F w u) (F' z u) z) :  HasDerivAt (fun z => ∫ u in Ioi (1 : ℝ), F z u) (∫ u in Ioi (1 : ℝ), F' s u) s := by  have h :=    hasDerivAt_integral_of_dominated_loc_of_deriv_le      (μ := volume.restrict (Ioi (1 : ℝ))) (F := F) (F' := F') (x₀ := s)      (s := Metric.ball s δ) (bound := bound) (Metric.ball_mem_nhds s hδ)      (hF_meas := hmeas) (hF_int := hFint) (hF'_meas := hF'meas)      (h_bound := hbound) (bound_integrable := hbound_int) (h_diff := hderiv)  rcases h with ⟨_, hDeriv⟩  exact hDeriv