ZetaAbelFractKernel.integral_analytic

theorem integral_analytic (s : ℂ) (hs : 0 < s.re) :    AnalyticAt ℂ (fun z => ∫ u in Ioi (1 : ℝ), zetaAbelFractKernel z u) s := by  set ε : ℝ := s.re / 2  have hεpos : 0 < ε := half_pos hs  obtain ⟨δ, hδpos, hδprop⟩ :=    Complex.exists_pos_radius_forall_mem_ball_re_ge (z₀ := s) (a := ε) (half_lt_self hs)  set F : ℂ → ℝ → ℂ := zetaAbelFractKernel  set F' : ℂ → ℝ → ℂ := fun z u => -((Real.log u) : ℂ) * F z u  set bound : ℝ → ℝ := fun u => (2 / ε) * u ^ (-1 - ε / 2)  have hbound_int : Integrable bound (volume.restrict (Ioi (1 : ℝ))) := by    simpa [bound, IntegrableOn] using      (integrableOn_Ioi_rpow_of_lt (by linarith [half_pos hεpos]) one_pos).const_mul (2 / ε)  have hDiff : ∀ᶠ z in 𝓝 s, DifferentiableAt ℂ (fun z0 => ∫ u in Ioi (1 : ℝ), F z0 u) z := by    refine Filter.eventually_of_mem (Metric.ball_mem_nhds s (half_pos hδpos)) ?_    intro z hz    set δ' : ℝ := δ / 2    have hz_lt : dist z s < δ := dist_lt_of_mem_ball_half hz hδpos    have hRe : ∀ y ∈ Metric.ball z δ', ε ≤ y.re := fun y hy =>      hδprop z y hz_lt (dist_lt_of_mem_ball_half hy hδpos)    have hzRe : ε ≤ z.re := hδprop s z (by simpa [dist_self] using hδpos) hz_lt    exact (hasDerivAt_integral_param_dominated_Ioi F F' z δ' (half_pos hδpos)      (eventually_aestronglyMeasurable_param z)      (by simpa using integrableOn_Ioi z (lt_of_lt_of_le hεpos hzRe))      (by simpa [F, F'] using aestronglyMeasurable_param_deriv z)      bound hbound_int      (ae_on_Ioi_of_all fun u hu w hw =>        (kernel_deriv_norm_bound_on_ball ε u hu w (hRe w hw)).trans          (by simpa [bound] using Real.log_mul_rpow_neg_le_two_div_mul_rpow_neg hεpos hu))      (ae_on_Ioi_of_all fun u hu w hw => by simpa [F, F'] using hasDerivAt_in_param u hu w)).differentiableAt  exact (Complex.analyticAt_iff_eventually_differentiableAt    (f := fun z => ∫ u in Ioi (1 : ℝ), zetaAbelFractKernel z u)).2 hDiff