Schwarz reflection of a conformal map is conformal

Conformal/Reflection/Principle.lean extends a function holomorphic on the upper part of a conjugation-symmetric open set Ω and real on Ω ∩ ℝ to a function holomorphic on all of Ω. This file upgrades that extension from holomorphic to conformal: if the original map is injective on the closed upper part and sends the open upper part into the open upper half-plane, then the reflected extension schwarzReflection f is injective on all of Ω — hence conformal at every point of Ω, with a holomorphic inverse on its image.

This is the form layer L5 of ConformalMapping/README.md consumes: the boundary correspondence extends a Riemann map across an analytic boundary arc by reflecting it, and what that step needs is not merely a holomorphic continuation but a conformal one — a continuation that is again injective, and whose derivative therefore does not vanish on the boundary arc itself. That last point is the payoff: f is not assumed differentiable at the real points of Ω at all, only continuous there from above, yet conformalAt_schwarzReflection_of_symmetric produces a nonvanishing derivative there for the extension.

The proof

Purely a matter of which half-plane each branch lands in, once the sign bookkeeping is recorded:

• on Ω ∩ {0 < im} the extension is f, which lands in {0 < im} by hypothesis;
• on Ω ∩ ℝ the extension is f, which is real by hypothesis — for injectivity alone only the weaker 0 ≤ (f z).im is used there;
• on Ω ∩ {im < 0} the extension is conj ∘ f ∘ conj, and conjugation twice reverses the sign of the imaginary part, so it lands in {im < 0}.

So the two branches have images in the two open half-planes and cannot collide with each other; a coincidence of values must therefore happen inside one branch, where injectivity of f on the closed upper part settles it — directly on the upper branch, and after cancelling the two conjugations on the lower one. The strictness of 0 < (f z).im for 0 < z.im is what separates the branches, and it is genuinely needed: without it f could map an interior point to the real axis, where the two branches meet.

The reflection hypotheses here are exactly those of the reflection principle, plus the two extra ones (hupper and hinj); the holomorphy of the extension is quoted from differentiableOn_schwarzReflection_of_symmetric, its pointwise conformality from DifferentiableOn.conformalAt_of_isOpen_of_injOn, and the holomorphy of the inverse from DifferentiableOn.invFunOn.

Main results

• TauCeti.injOn_schwarzReflection_of_symmetric — the reflected extension of an injective map is injective.
• TauCeti.image_schwarzReflection_of_symmetric — its image is the image of the closed upper part together with the mirror image of that set.
• TauCeti.deriv_schwarzReflection_ne_zero — its derivative vanishes nowhere on Ω, in particular on the boundary segment Ω ∩ ℝ.
• TauCeti.conformalAt_schwarzReflection_of_symmetric — the extension is conformal at every point of Ω, including the points of the real axis.
• TauCeti.differentiableOn_invFunOn_schwarzReflection_of_symmetric — its inverse is holomorphic, so the extension is a biholomorphism onto its image.
• TauCeti.exists_differentiableOn_injOn_eqOn_conj_of_symmetric — the packaged form: a conformal map of the upper part extends to a conformal map of Ω obeying the reflection symmetry.

Coordination with upstream Mathlib

Layer L4 (reflection) and layer L5 (boundary correspondence) are absent from the in-progress Mathlib Riemann-mapping draft mathlib4#33505, so this is new Lean formalization rather than a shim; the shared L0--L3 infrastructure it consumes (Conformal/Biholomorph.lean, Conformal/Inverse/Function.lean) carries its own shim notice.

References

• L. Ahlfors, Complex Analysis, Ch. 6.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 1--3.

theorem TauCeti.mapsTo_schwarzReflection_im_pos {Ω : Set ℂ} {f : ℂ → ℂ} (hupper : Set.MapsTo f (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}) : Set.MapsTo (schwarzReflection f) (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}

On the open upper part of the domain the reflection extension is the original map, so it inherits the hypothesis that f takes the open upper part into the open upper half-plane.

theorem TauCeti.mapsTo_schwarzReflection_im_neg {Ω : Set ℂ} {f : ℂ → ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hupper : Set.MapsTo f (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}) : Set.MapsTo (schwarzReflection f) (Ω ∩ {z : ℂ | z.im < 0}) {z : ℂ | z.im < 0}

The reflected branch takes the lower part of a conjugation-symmetric domain into the open lower half-plane: it conjugates a value of f at a point of the open upper part, and conjugation reverses the sign of the imaginary part.

theorem TauCeti.im_schwarzReflection_nonneg {Ω : Set ℂ} {f : ℂ → ℂ} (hupper : Set.MapsTo f (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}) (haxis : ∀ z ∈ Ω, z.im = 0 → 0 ≤ (f z).im) {z : ℂ} (hz : z ∈ Ω) (hzim : 0 ≤ z.im) : 0 ≤ (schwarzReflection f z).im

On the closed upper part the extension has nonnegative imaginary part: positive above the axis, and nonnegative on it. Only nonnegativity of (f z).im on the axis is needed, not the reflection principle's stronger (f z).im = 0.

theorem TauCeti.injOn_schwarzReflection_of_symmetric {Ω : Set ℂ} {f : ℂ → ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hupper : Set.MapsTo f (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}) (haxis : ∀ z ∈ Ω, z.im = 0 → 0 ≤ (f z).im) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) : Set.InjOn (schwarzReflection f) Ω

Schwarz reflection preserves injectivity. On a conjugation-symmetric open set Ω, if f is injective on the closed upper part, has nonnegative imaginary part on Ω ∩ ℝ, and maps the open upper part into the open upper half-plane, then the reflection extension schwarzReflection f is injective on all of Ω.

The two branches take values in the two open half-planes, so they cannot meet; within a single branch the injectivity of f applies, on the lower branch after cancelling the conjugations.

Injectivity alone does not need f to be real on the axis, only to stay in the closed upper half-plane there; the corollaries below feed haxis from the reflection principle's hreal.

theorem TauCeti.image_schwarzReflection_of_symmetric {Ω : Set ℂ} {f : ℂ → ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) : schwarzReflection f '' Ω = f '' (Ω ∩ {z : ℂ | 0 ≤ z.im}) ∪ ⇑(starRingEnd ℂ) '' f '' (Ω ∩ {z : ℂ | 0 ≤ z.im})

The image of the reflection extension is the image of the closed upper part together with its mirror image in the real axis. The real axis contributes to both pieces, since f is real there.

theorem TauCeti.deriv_schwarzReflection_ne_zero {Ω : Set ℂ} {f : ℂ → ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) (hupper : Set.MapsTo f (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) {z : ℂ} (hz : z ∈ Ω) : deriv (schwarzReflection f) z ≠ 0

The reflected map has nonvanishing derivative on the boundary segment. Under the hypotheses of the reflection principle, together with injectivity of f on the closed upper part and the requirement that the open upper part goes to the open upper half-plane, the derivative of the extension vanishes nowhere on Ω. At a point of Ω ∩ ℝ this is a statement about the boundary behaviour of f, which is not assumed differentiable there.

theorem TauCeti.conformalAt_schwarzReflection_of_symmetric {Ω : Set ℂ} {f : ℂ → ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) (hupper : Set.MapsTo f (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) {z : ℂ} (hz : z ∈ Ω) : ConformalAt (schwarzReflection f) z

Schwarz reflection of a conformal map is conformal. Under the hypotheses of the reflection principle, together with injectivity of f on the closed upper part and the requirement that the open upper part goes to the open upper half-plane, the extension is conformal at every point of Ω — in particular at the points of the real axis, where f itself is not assumed differentiable.

theorem TauCeti.differentiableOn_invFunOn_schwarzReflection_of_symmetric {Ω : Set ℂ} {f : ℂ → ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) (hupper : Set.MapsTo f (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) : DifferentiableOn ℂ (Function.invFunOn (schwarzReflection f) Ω) (schwarzReflection f '' Ω)

The inverse of the reflection extension is holomorphic on its image: the extension is a biholomorphism of Ω onto the doubled image described by image_schwarzReflection_of_symmetric.

theorem TauCeti.exists_differentiableOn_injOn_eqOn_conj_of_symmetric {Ω : Set ℂ} {f : ℂ → ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) (hupper : Set.MapsTo f (Ω ∩ {z : ℂ | 0 < z.im}) {z : ℂ | 0 < z.im}) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) : ∃ (F : ℂ → ℂ), DifferentiableOn ℂ F Ω ∧ Set.InjOn F Ω ∧ Set.EqOn F f (Ω ∩ {z : ℂ | 0 ≤ z.im}) ∧ ∀ z ∈ Ω, F ((starRingEnd ℂ) z) = (starRingEnd ℂ) (F z)

The conformal reflection principle, packaged existential form: a conformal map of the upper part of a conjugation-symmetric open set that is real on the axis and takes the open upper part into the open upper half-plane extends to a conformal map of the whole set, agreeing with the original on the closed upper part and obeying the reflection symmetry F (conj z) = conj (F z). The explicit witness is schwarzReflection f.

This strengthens exists_differentiableOn_eqOn_conj_of_symmetric by the injectivity clause.