Painlevé removability across an analytic arc

An analytic arc is locally straightened by a biholomorphic coordinate chart. This file proves that every subset of the real locus of such a chart is removable for continuous holomorphic functions: if F is continuous on an open part of the chart source and holomorphic away from the subset, then F is holomorphic throughout that open set.

The proof reads F in the chart coordinate as F ∘ e.symm. The inverse chart is holomorphic on the image of the domain by DifferentiableOn.invFunOn, and the removable set becomes a subset of the real axis. Painlevé removability of the real axis then applies, after which the result is transported back through e.

This is the analytic-arc case requested by layer L4 of the conformal-mapping roadmap. It follows the standard coordinate reduction of removability across an analytic arc to the real axis; see Ahlfors, Complex Analysis, Chapter 6, §1.4, and Rudin, Real and Complex Analysis, Chapter 11, Exercise 11.

Main results

• TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_of_subset_coord_im_eq_zero: every subset of the charted real locus is removable.
• TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_coord_im_eq_zero: removability of the full charted real locus.
• The corresponding gluing theorem for the two sides of the arc.

theorem TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_of_subset_coord_im_eq_zero {F : ℂ → ℂ} (e : OpenPartialHomeomorph ℂ ℂ) {Ω S : Set ℂ} (he : DifferentiableOn ℂ (↑e) Ω) (hΩ : IsOpen Ω) (hΩe : Ω ⊆ e.source) (hcont : ContinuousOn F Ω) (hdiff : DifferentiableOn ℂ F (Ω \ S)) (hS : Ω ∩ S ⊆ {z : ℂ | (↑e z).im = 0}) : DifferentiableOn ℂ F Ω

Painlevé removability across a charted analytic arc. Let e be an open partial homeomorphism of ℂ that is holomorphic on an open subset Ω of its source, and let S meet Ω only where the chart coordinate is real. A function continuous on Ω and holomorphic there away from S is holomorphic throughout Ω.

The hypothesis on S only constrains its intersection with Ω, since points outside the domain under consideration do not affect the conclusion.

theorem TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_diff_coord_im_eq_zero {F : ℂ → ℂ} (e : OpenPartialHomeomorph ℂ ℂ) {Ω : Set ℂ} (he : DifferentiableOn ℂ (↑e) Ω) (hΩ : IsOpen Ω) (hΩe : Ω ⊆ e.source) (hcont : ContinuousOn F Ω) (hdiff : DifferentiableOn ℂ F (Ω \ {z : ℂ | (↑e z).im = 0})) : DifferentiableOn ℂ F Ω

Painlevé removability of the full real locus of a holomorphic chart. If a function is continuous on an open part of the chart source and holomorphic wherever the chart coordinate has nonzero imaginary part, then it is holomorphic throughout that open set.

theorem TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_coord_im_pos_of_differentiableOn_coord_im_neg {F : ℂ → ℂ} (e : OpenPartialHomeomorph ℂ ℂ) {Ω : Set ℂ} (he : DifferentiableOn ℂ (↑e) Ω) (hΩ : IsOpen Ω) (hΩe : Ω ⊆ e.source) (hcont : ContinuousOn F Ω) (hpos : DifferentiableOn ℂ F (Ω ∩ {z : ℂ | 0 < (↑e z).im})) (hneg : DifferentiableOn ℂ F (Ω ∩ {z : ℂ | (↑e z).im < 0})) : DifferentiableOn ℂ F Ω

Gluing across a charted analytic arc. A continuous function on an open part of the source of a holomorphic chart that is holomorphic on both open sides of the charted real locus is holomorphic throughout that open set.