Painlevé removability across a circle #
A circle is a removable set for continuous holomorphic functions: if F is continuous on an open
set Ω ⊆ ℂ and holomorphic on Ω off a positive-radius circle, then F is holomorphic on all of
Ω.
The proof reduces to Painlevé removability of the real axis from
Conformal/Removability/Basic.lean. Two fractional-linear charts cover the circle, with each
chart carrying the real axis to the circle and omitting one point.
theorem
TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_sphere
{Ω : Set ℂ}
{F : ℂ → ℂ}
{c : ℂ}
{r : ℝ}
(hr : 0 < r)
(hΩ : IsOpen Ω)
(hcont : ContinuousOn F Ω)
(hdiff : DifferentiableOn ℂ F (Ω \ Metric.sphere c r))
:
DifferentiableOn ℂ F Ω
Painlevé removability across a circle. A function continuous on an open set Ω ⊆ ℂ
and holomorphic off a positive-radius circle is holomorphic throughout Ω.