Conjugating a holomorphic map by circle reflections

This file develops the analytic operation used to transport Schwarz reflection from a line to a circle. Given source and target circles, circleReflectionConjugate reflects the argument in the source circle, applies a map, and reflects its value in the target circle. Although each circle reflection is antiholomorphic, their composite around a holomorphic map is holomorphic away from the source centre and points mapped to the target centre.

The main result, differentiableOn_circleReflectionConjugate, proves this holomorphy transfer on an arbitrary set. The proof reduces circle inversion to conjugation followed by a holomorphic fractional-linear coordinate, then uses the conjugation-composition lemma from Reflection/Basic.lean. The accompanying involution theorem records that applying the operation again recovers the original map when both radii are nonzero.

This is a prerequisite for the circle case of layer L4 in the conformal-mapping roadmap: Schwarz reflection "across an analytic arc / circle by Möbius reduction". The construction follows the standard circle-reflection formula; see Ahlfors, Complex Analysis, Chapters 4--6. This L4 material is absent from the upstream Mathlib Riemann-mapping draft mathlib4#33505.

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

Conjugate a map by reflections in a source circle and a target circle.

The source circle has centre c and radius r, and the target circle has centre d and radius s. Thus the value at z is R_{d,s} (f (R_{c,r} z)), where R denotes Euclidean inversion. The definition is total; analytic results exclude the centres where the inversion formula has a pole.

Equations

• TauCeti.circleReflectionConjugate c r d s f z = EuclideanGeometry.inversion d s (f (EuclideanGeometry.inversion c r z))

@[simp]

theorem TauCeti.circleReflectionConjugate_apply (c : ℂ) (r : ℝ) (d : ℂ) (s : ℝ) (f : ℂ → ℂ) (z : ℂ) : circleReflectionConjugate c r d s f z = EuclideanGeometry.inversion d s (f (EuclideanGeometry.inversion c r z))

The circle-reflection conjugate is the composite of the two inversions and the map.

@[simp]

theorem TauCeti.circleReflectionConjugate_zero_source_radius (c d : ℂ) (s : ℝ) (f : ℂ → ℂ) : circleReflectionConjugate c 0 d s f = fun (x : ℂ) => EuclideanGeometry.inversion d s (f c)

With zero source radius, the circle-reflection conjugate is constant.

@[simp]

theorem TauCeti.circleReflectionConjugate_zero_target_radius (c : ℂ) (r : ℝ) (d : ℂ) (f : ℂ → ℂ) : circleReflectionConjugate c r d 0 f = fun (x : ℂ) => d

With zero target radius, the circle-reflection conjugate is constant.

theorem TauCeti.circleReflectionConjugate_eqOn_sphere (c : ℂ) (r : ℝ) (d : ℂ) (s : ℝ) (f : ℂ → ℂ) (hmap : Set.MapsTo f (Metric.sphere c r) (Metric.sphere d s)) : Set.EqOn (circleReflectionConjugate c r d s f) f (Metric.sphere c r)

The circle-reflection conjugate agrees with the original map on the source circle when the map sends the source circle into the target circle.

@[simp]

theorem TauCeti.circleReflectionConjugate_circleReflectionConjugate (c : ℂ) {r : ℝ} (d : ℂ) {s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) (f : ℂ → ℂ) : circleReflectionConjugate c r d s (circleReflectionConjugate c r d s f) = f

Applying the same circle-reflection conjugation twice recovers the original map.

theorem TauCeti.differentiableOn_circleReflectionConjugate {c : ℂ} {r : ℝ} {d : ℂ} {s : ℝ} {f : ℂ → ℂ} {Ω S : Set ℂ} (hf : r ≠ 0 ∧ s ≠ 0 → DifferentiableOn ℂ f Ω) (hmap : r ≠ 0 ∧ s ≠ 0 → Set.MapsTo (EuclideanGeometry.inversion c r) S Ω) (hc : r ≠ 0 ∧ s ≠ 0 → c ∉ S) (hd : r ≠ 0 ∧ s ≠ 0 → ∀ z ∈ S, f (EuclideanGeometry.inversion c r z) ≠ d) : DifferentiableOn ℂ (circleReflectionConjugate c r d s f) S

Conjugating a holomorphic map by source and target circle reflections is holomorphic away from the inversion centres.

When both radii are nonzero, the set S is mapped into the original holomorphy domain Ω by source reflection, and the two nonincidence hypotheses remove the poles of the source and target inversions. These hypotheses are unnecessary when either radius is zero, since the conjugate is then constant.