The Schwarz reflection principle across a circle

This file proves the circle case of the Schwarz reflection principle. A continuous function holomorphic on one side of a circle and taking that circle into another circle extends across the source circle by conjugating it with the two circle inversions. The extension is holomorphic wherever the reflected branch avoids the target centre.

The analytic gluing step is Painlevé removability for a circle, supplied by Conformal/Removability/Circle.lean. This is the Möbius-reduction route specified by layer L4 of the conformal-mapping roadmap.

The construction follows Ahlfors, Complex Analysis, Chapters 4--6. It reuses Mathlib's topological piecewise API and Euclidean inversion, together with Tau Ceti's line-removability and circle-reflection conjugation theorems. Layer L4 is absent from the upstream Mathlib Riemann-mapping draft mathlib4#33505.

noncomputable def TauCeti.circleSchwarzReflection (c : ℂ) (r : ℝ) (d : ℂ) (s : ℝ) (f : ℂ → ℂ) (z : ℂ) : ℂ

The explicit extension used for Schwarz reflection across a circle. Inside the closed source disc it is f; outside it is f conjugated by reflection in the source and target circles.

Equations

• TauCeti.circleSchwarzReflection c r d s f z = (Metric.closedBall c r).piecewise f (TauCeti.circleReflectionConjugate c r d s f) z

theorem TauCeti.circleSchwarzReflection_def (c : ℂ) (r : ℝ) (d : ℂ) (s : ℝ) (f : ℂ → ℂ) : circleSchwarzReflection c r d s f = (Metric.closedBall c r).piecewise f (circleReflectionConjugate c r d s f)

The circle Schwarz-reflection extension is the explicit inside/outside piecewise function.

@[simp]

theorem TauCeti.circleSchwarzReflection_of_mem_closedBall {c : ℂ} {r : ℝ} (d : ℂ) (s : ℝ) (f : ℂ → ℂ) {z : ℂ} (hz : z ∈ Metric.closedBall c r) : circleSchwarzReflection c r d s f z = f z

On the closed source disc, the circle-reflection extension agrees with the original map.

@[simp]

theorem TauCeti.circleSchwarzReflection_of_notMem_closedBall (c : ℂ) (r : ℝ) (d : ℂ) (s : ℝ) (f : ℂ → ℂ) {z : ℂ} (hz : z ∉ Metric.closedBall c r) : circleSchwarzReflection c r d s f z = circleReflectionConjugate c r d s f z

Outside the closed source disc, the extension is the circle-reflection conjugate.

theorem TauCeti.continuousOn_circleSchwarzReflection_of_symmetric {Ω : Set ℂ} {c d : ℂ} {r s : ℝ} {f : ℂ → ℂ} (hr : 0 < r) (hs : 0 < s) (hsymm : Set.MapsTo (EuclideanGeometry.inversion c r) Ω Ω) (hcont : ContinuousOn f (Ω ∩ Metric.closedBall c r)) (hboundary : Set.MapsTo f (Ω ∩ Metric.sphere c r) (Metric.sphere d s)) (havoid : ∀ z ∈ Ω ∩ Metric.ball c r, z ≠ c → f z ≠ d) : ContinuousOn (circleSchwarzReflection c r d s f) Ω

If Ω is mapped into itself by inversion in the source circle, the circle-reflection extension is continuous when the original map is continuous on the closed inside part, maps the source-circle boundary to the target circle, and avoids the target centre in the punctured open inside part.

theorem TauCeti.differentiableOn_circleSchwarzReflection_of_symmetric {Ω : Set ℂ} {c d : ℂ} {r s : ℝ} {f : ℂ → ℂ} (hr : 0 < r) (hs : 0 < s) (hΩ : IsOpen Ω) (hsymm : Set.MapsTo (EuclideanGeometry.inversion c r) Ω Ω) (hcont : ContinuousOn f (Ω ∩ Metric.closedBall c r)) (hholo : DifferentiableOn ℂ f (Ω ∩ Metric.ball c r)) (hboundary : Set.MapsTo f (Ω ∩ Metric.sphere c r) (Metric.sphere d s)) (havoid : ∀ z ∈ Ω ∩ Metric.ball c r, z ≠ c → f z ≠ d) : DifferentiableOn ℂ (circleSchwarzReflection c r d s f) Ω

Schwarz reflection principle across a circle. Let Ω be an open set invariant under reflection in the source circle. If f is continuous on the closed inside part, holomorphic on the open inside part, sends the source-circle boundary into the target circle, and avoids the target centre in the punctured interior, then its explicit circle-reflection extension is holomorphic throughout Ω.

The target-centre avoidance is exactly the non-pole condition for reflection in the target circle.