Identity theorem on a right half-plane #
Holomorphic functions on Re s > a that agree on a smaller right half-plane Re s > b,
where a < b, agree throughout Re s > a.
theorem
TauCeti.eq_of_differentiableOn_of_eq_on_halfPlane
{f g : ℂ → ℂ}
{a b : ℝ}
(hab : a < b)
(hf : DifferentiableOn ℂ f {s : ℂ | a < s.re})
(hg : DifferentiableOn ℂ g {s : ℂ | a < s.re})
(hfg : ∀ (s : ℂ), b < s.re → f s = g s)
{s : ℂ}
(hs : a < s.re)
:
Two functions holomorphic on Re s > a that agree on Re s > b, for a < b,
agree throughout Re s > a.