The Schwarz reflection principle across an affine line

This file transports the real-axis Schwarz reflection principle through complex affine charts. For a base point p and a nonzero direction a, the chart w ↦ p + a * w carries the real axis to the affine line through p in direction a. Applying such a chart in both source and target gives the explicit extension lineSchwarzReflection.

The main theorem, differentiableOn_lineSchwarzReflection_of_symmetric, proves that this extension is holomorphic on a domain invariant under reflection in the source line. The hypotheses say that the original branch is continuous and holomorphic on one side of the line and maps its boundary values into the target line. The accompanying branch and symmetry lemmas characterize the extension without requiring consumers to unfold its definition.

This is the straight-arc case of layer L4 in the conformal-mapping roadmap, which asks for Schwarz reflection across an analytic arc or circle by Möbius reduction. The construction follows the standard affine reduction to the real-axis principle; see Ahlfors, Complex Analysis, Chapters 4--6. Layer L4 is absent from the upstream Mathlib Riemann-mapping draft leanprover-community/mathlib4#33505.

noncomputable def TauCeti.lineSchwarzReflection (p a q b : ℂ) (f : ℂ → ℂ) (z : ℂ) : ℂ

The explicit Schwarz-reflection extension across affine source and target lines.

The source line has base point p and direction a, while the target line has base point q and direction b. In affine coordinates, this is exactly the real-axis extension: q + b * schwarzReflection (w ↦ (f (p + a * w) - q) / b) ((z - p) / a). The definition is total. Agreement with the original branch and the reflection symmetry assume a ≠ 0 and b ≠ 0; holomorphy itself only needs a ≠ 0, since b = 0 makes the function constant.

Equations

• TauCeti.lineSchwarzReflection p a q b f z = q + b * TauCeti.schwarzReflection (fun (w : ℂ) => (f (p + a * w) - q) / b) ((z - p) / a)

theorem TauCeti.lineSchwarzReflection_def (p a q b : ℂ) (f : ℂ → ℂ) (z : ℂ) : lineSchwarzReflection p a q b f z = q + b * schwarzReflection (fun (w : ℂ) => (f (p + a * w) - q) / b) ((z - p) / a)

The affine-line Schwarz-reflection extension in source and target coordinates.

@[simp]

theorem TauCeti.lineSchwarzReflection_of_coord_im_nonneg {p a q b z : ℂ} (f : ℂ → ℂ) (ha : a ≠ 0) (hb : b ≠ 0) (hz : 0 ≤ ((z - p) / a).im) : lineSchwarzReflection p a q b f z = f z

On the closed positive side of the source line, affine-line Schwarz reflection agrees with the original function.

@[simp]

theorem TauCeti.lineSchwarzReflection_of_coord_im_neg {p a q b z : ℂ} (f : ℂ → ℂ) (hz : ((z - p) / a).im < 0) : lineSchwarzReflection p a q b f z = q + b * (starRingEnd ℂ) ((f (p + a * (starRingEnd ℂ) ((z - p) / a)) - q) / b)

On the negative side of the source line, affine-line Schwarz reflection is obtained by reflecting the argument in the source line and the value in the target line.

theorem TauCeti.differentiableOn_lineSchwarzReflection_of_symmetric {Ω : Set ℂ} {p a q b : ℂ} {f : ℂ → ℂ} (ha : a ≠ 0) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (fun (z : ℂ) => p + a * (starRingEnd ℂ) ((z - p) / a)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ ((z - p) / a).im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < ((z - p) / a).im})) (hline : ∀ z ∈ Ω, ((z - p) / a).im = 0 → ((f z - q) / b).im = 0) : DifferentiableOn ℂ (lineSchwarzReflection p a q b f) Ω

Schwarz reflection principle across an affine line, holomorphy form. Let the source line be p + a * ℝ, with a ≠ 0. Suppose an open domain Ω is invariant under reflection in this line. If f is continuous on the closed positive side, holomorphic on the open positive side, and its boundary values have real target coordinate, then lineSchwarzReflection p a q b f is holomorphic throughout Ω.

The side and boundary conditions are expressed in the affine coordinates (z - p) / a and (f z - q) / b. The target direction b need not be nonzero for holomorphy: when b = 0, the conclusion is the constant function with value q. The packaged reflection theorem below assumes b ≠ 0 to obtain branch agreement and target-line symmetry.

theorem TauCeti.lineSchwarzReflection_sourceReflection {Ω : Set ℂ} {p a q b : ℂ} {f : ℂ → ℂ} (ha : a ≠ 0) (hb : b ≠ 0) (hline : ∀ z ∈ Ω, ((z - p) / a).im = 0 → ((f z - q) / b).im = 0) {z : ℂ} (hz : z ∈ Ω) : lineSchwarzReflection p a q b f (p + a * (starRingEnd ℂ) ((z - p) / a)) = q + b * (starRingEnd ℂ) ((lineSchwarzReflection p a q b f z - q) / b)

Affine-line Schwarz reflection intertwines reflection in the source line with reflection in the target line. The boundary hypothesis says precisely that the original function takes the source line into the target line.

theorem TauCeti.exists_differentiableOn_eqOn_lineReflection_of_symmetric {Ω : Set ℂ} {p a q b : ℂ} {f : ℂ → ℂ} (ha : a ≠ 0) (hb : b ≠ 0) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (fun (z : ℂ) => p + a * (starRingEnd ℂ) ((z - p) / a)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ ((z - p) / a).im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < ((z - p) / a).im})) (hline : ∀ z ∈ Ω, ((z - p) / a).im = 0 → ((f z - q) / b).im = 0) : ∃ (F : ℂ → ℂ), DifferentiableOn ℂ F Ω ∧ Set.EqOn F f (Ω ∩ {z : ℂ | 0 ≤ ((z - p) / a).im}) ∧ ∀ z ∈ Ω, F (p + a * (starRingEnd ℂ) ((z - p) / a)) = q + b * (starRingEnd ℂ) ((F z - q) / b)

Schwarz reflection principle across affine source and target lines, packaged form. Under the hypotheses of differentiableOn_lineSchwarzReflection_of_symmetric, with both line directions nonzero, there is a holomorphic extension which agrees with f on the closed positive side and intertwines reflection in the source and target lines. The witness is the explicit function lineSchwarzReflection p a q b f.