Holomorphic continuation to a neighbourhood of a closed half-plane

Tauberian theorems at the boundary of a half-plane, such as Newman's, ask for a function that is holomorphic on some open set containing the closed half-plane σ ≤ re s. When the function is already holomorphic on the open half-plane σ < re s, for example because it is a Laplace transform or a Dirichlet series there, this hypothesis only concerns the boundary line: it holds exactly when the function is analytic at every point of re s = σ (TauCeti.exists_isOpen_differentiableOn_iff_analyticAt). The open set can then be taken to be the set of points at which the function is analytic, which is open by Mathlib's isOpen_analyticAt.

theorem TauCeti.exists_isOpen_differentiableOn_iff_analyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {F : ℂ → E} {σ : ℝ} (hF : DifferentiableOn ℂ F {s : ℂ | σ < s.re}) : (∃ (Ω : Set ℂ), IsOpen Ω ∧ {s : ℂ | σ ≤ s.re} ⊆ Ω ∧ DifferentiableOn ℂ F Ω) ↔ ∀ (s : ℂ), s.re = σ → AnalyticAt ℂ F s

A function holomorphic on the open half-plane σ < re s is holomorphic on an open set containing the closed half-plane σ ≤ re s if and only if it is analytic at every point of the boundary line re s = σ.