The Schwarz reflection principle across an analytic arc

This file transports the real-axis Schwarz reflection principle through biholomorphic coordinate charts. An OpenPartialHomeomorph ℂ ℂ whose forward map is holomorphic on its source is a biholomorphic chart: injectivity and the holomorphic inverse theorem make its inverse holomorphic on the target. The inverse image of the real axis under such a chart is therefore locally a real-analytic arc.

For source and target charts e and d, chartedSchwarzReflection e d f straightens the source arc with e, applies d to the values, uses real-axis reflection in the two coordinate domains, and then maps back with d.symm. The coordinate domains are assumed invariant under conjugation. The main theorem proves that this explicit extension is holomorphic throughout e.source; its packaged form also records agreement with the original branch and the induced reflection symmetry.

This proves the analytic-arc part of layer L4 in the conformal-mapping roadmap. It follows the standard reduction of reflection across an analytic arc to reflection across the real axis; see Ahlfors, Complex Analysis, Chapters 4--6. The underlying real-axis theorem is TauCeti.differentiableOn_schwarzReflection_of_symmetric.

noncomputable def TauCeti.chartedSchwarzReflection (e d : OpenPartialHomeomorph ℂ ℂ) (f : ℂ → ℂ) (z : ℂ) : ℂ

The Schwarz-reflection extension transported through source and target biholomorphic charts.

The source chart e straightens the source arc, and the target chart d straightens the target arc. Thus the middle function in real-axis coordinates is w ↦ d (f (e.symm w)). The definition is total, while its characteristic properties only concern the sources and targets of the two partial homeomorphisms.

Equations

• TauCeti.chartedSchwarzReflection e d f z = ↑d.symm (TauCeti.schwarzReflection (fun (w : ℂ) => ↑d (f (↑e.symm w))) (↑e z))

theorem TauCeti.chartedSchwarzReflection_def (e d : OpenPartialHomeomorph ℂ ℂ) (f : ℂ → ℂ) (z : ℂ) : chartedSchwarzReflection e d f z = ↑d.symm (schwarzReflection (fun (w : ℂ) => ↑d (f (↑e.symm w))) (↑e z))

The defining formula for Schwarz reflection transported through biholomorphic charts.

theorem TauCeti.mapsTo_chartedSchwarzReflection (e d : OpenPartialHomeomorph ℂ ℂ) (f : ℂ → ℂ) (he_symm : Set.MapsTo (⇑(starRingEnd ℂ)) e.target e.target) (hd_symm : Set.MapsTo (⇑(starRingEnd ℂ)) d.target d.target) (hf : Set.MapsTo f (e.source ∩ {z : ℂ | 0 ≤ (↑e z).im}) d.source) : Set.MapsTo (chartedSchwarzReflection e d f) e.source d.source

Charted Schwarz reflection maps the source chart domain into the target chart domain.

@[simp]

theorem TauCeti.chartedSchwarzReflection_of_coord_im_nonneg (e d : OpenPartialHomeomorph ℂ ℂ) (f : ℂ → ℂ) (hf : Set.MapsTo f (e.source ∩ {z : ℂ | 0 ≤ (↑e z).im}) d.source) {z : ℂ} (hz : z ∈ e.source) (him : 0 ≤ (↑e z).im) : chartedSchwarzReflection e d f z = f z

On the closed positive side of the source arc, charted Schwarz reflection agrees with the original function.

@[simp]

theorem TauCeti.chartedSchwarzReflection_of_coord_im_neg (e d : OpenPartialHomeomorph ℂ ℂ) (f : ℂ → ℂ) {z : ℂ} (him : (↑e z).im < 0) : chartedSchwarzReflection e d f z = ↑d.symm ((starRingEnd ℂ) (↑d (f (↑e.symm ((starRingEnd ℂ) (↑e z))))))

On the negative side of the source arc, charted Schwarz reflection is obtained by reflecting the argument and value in the two coordinate charts.

theorem TauCeti.differentiableOn_chartedSchwarzReflection_of_symmetric (e d : OpenPartialHomeomorph ℂ ℂ) (f : ℂ → ℂ) (he : DifferentiableOn ℂ (↑e) e.source) (hd : DifferentiableOn ℂ (↑d) d.source) (he_symm : Set.MapsTo (⇑(starRingEnd ℂ)) e.target e.target) (hd_symm : Set.MapsTo (⇑(starRingEnd ℂ)) d.target d.target) (hf_maps : Set.MapsTo f (e.source ∩ {z : ℂ | 0 ≤ (↑e z).im}) d.source) (hf_cont : ContinuousOn f (e.source ∩ {z : ℂ | 0 ≤ (↑e z).im})) (hf_diff : DifferentiableOn ℂ f (e.source ∩ {z : ℂ | 0 < (↑e z).im})) (hf_real : ∀ z ∈ e.source, (↑e z).im = 0 → (↑d (f z)).im = 0) : DifferentiableOn ℂ (chartedSchwarzReflection e d f) e.source

Schwarz reflection across an analytic arc. Let e and d be holomorphic open partial homeomorphisms whose coordinate domains are invariant under conjugation. If f is continuous on the closed positive side of the source arc, holomorphic on its open positive side, maps that side into the source of d, and maps the arc into the target arc, then its charted Schwarz-reflection extension is holomorphic throughout the source of e.

The source and target arcs are the inverse images of the real axis under e and d. Holomorphy of the inverse charts is a consequence of holomorphy and injectivity of their forward maps, so it is not imposed as an additional hypothesis.

theorem TauCeti.chartedSchwarzReflection_sourceReflection (e d : OpenPartialHomeomorph ℂ ℂ) (f : ℂ → ℂ) (he_symm : Set.MapsTo (⇑(starRingEnd ℂ)) e.target e.target) (hd_symm : Set.MapsTo (⇑(starRingEnd ℂ)) d.target d.target) (hf_maps : Set.MapsTo f (e.source ∩ {z : ℂ | 0 ≤ (↑e z).im}) d.source) (hf_real : ∀ z ∈ e.source, (↑e z).im = 0 → (↑d (f z)).im = 0) {z : ℂ} (hz : z ∈ e.source) : chartedSchwarzReflection e d f (↑e.symm ((starRingEnd ℂ) (↑e z))) = ↑d.symm ((starRingEnd ℂ) (↑d (chartedSchwarzReflection e d f z)))

Charted Schwarz reflection intertwines the source and target reflections induced by the two biholomorphic charts.

theorem TauCeti.exists_differentiableOn_eqOn_chartedReflection_of_symmetric (e d : OpenPartialHomeomorph ℂ ℂ) (f : ℂ → ℂ) (he : DifferentiableOn ℂ (↑e) e.source) (hd : DifferentiableOn ℂ (↑d) d.source) (he_symm : Set.MapsTo (⇑(starRingEnd ℂ)) e.target e.target) (hd_symm : Set.MapsTo (⇑(starRingEnd ℂ)) d.target d.target) (hf_maps : Set.MapsTo f (e.source ∩ {z : ℂ | 0 ≤ (↑e z).im}) d.source) (hf_cont : ContinuousOn f (e.source ∩ {z : ℂ | 0 ≤ (↑e z).im})) (hf_diff : DifferentiableOn ℂ f (e.source ∩ {z : ℂ | 0 < (↑e z).im})) (hf_real : ∀ z ∈ e.source, (↑e z).im = 0 → (↑d (f z)).im = 0) : ∃ (F : ℂ → ℂ), DifferentiableOn ℂ F e.source ∧ Set.EqOn F f (e.source ∩ {z : ℂ | 0 ≤ (↑e z).im}) ∧ ∀ z ∈ e.source, F (↑e.symm ((starRingEnd ℂ) (↑e z))) = ↑d.symm ((starRingEnd ℂ) (↑d (F z)))

Packaged Schwarz reflection across an analytic arc. Under the hypotheses of differentiableOn_chartedSchwarzReflection_of_symmetric, there is a holomorphic extension that agrees with the original function on the closed positive side and intertwines the source and target reflections induced by the charts. The witness is chartedSchwarzReflection e d f.