The pre-Schwarzian derivative along a straight boundary arc

A holomorphic function whose boundary values on a real interval run along an affine line continues across that interval by Schwarz reflection, and the continuation F intertwines conjugation with the reflection in the target line: F (conj z) = τ (F z). Every reflection in a line of direction b has the affine shape τ w = c + u * conj w with u = b / conj b, and this file draws out what that shape forces on the derivatives of F.

Differentiating the identity once removes the additive constant, so deriv F satisfies the same identity with c = 0; differentiating a second time leaves that identity unchanged. The factor u therefore cancels from the quotient deriv (deriv F) / deriv F, the pre-Schwarzian derivative logDeriv (deriv F), which obeys the bare conjugation symmetry logDeriv (deriv F) (conj z) = conj (logDeriv (deriv F) z) and is consequently real on the real axis. Nothing about the target line survives into that conclusion; only the source line is remembered. What the target line does control is deriv F itself, which on the real axis is a real multiple of the direction b: the boundary arc runs along the target line.

Differentiability of F is not needed for any of this. The identity is an equality between derivs, and deriv of a function that is not differentiable at a point is 0 there, which satisfies the identity as well.

These are the local statements the Schwarz--Christoffel formula needs in its converse direction. A conformal map of the upper half-plane onto a polygon carries each boundary interval between two consecutive prevertices into one side, hence has real pre-Schwarzian there. When the map is also injective up to that interval and sends the upper half-plane to one side of the side's line, the reflected extension is injective, so its derivative does not vanish on the interval and its pre-Schwarzian is holomorphic across it. Assembling those intervals, the pre-Schwarzian continues to a conjugation-symmetric function holomorphic on the plane minus the prevertices (TauCeti.exists_differentiableOn_eqOn_logDeriv_deriv). Reading off its poles at the prevertices is what identifies it with ∑ i, e i / (z - a i), the pre-Schwarzian derivative of the Schwarz--Christoffel map (TauCeti.logDeriv_deriv_schwarzChristoffelPrimitive).

The source line is the real axis throughout, as in TauCeti/Analysis/Complex/Conformal/Reflection/Basic.lean: unlike holomorphy, the pre-Schwarzian derivative is not invariant under an affine change of the source coordinate -- precomposing with w ↦ p + a * w multiplies it by a -- so a general source line would only move that factor into the statement, and the real axis is the coordinate the Schwarz--Christoffel prevertices live in. The target line is arbitrary, since a polygon's sides are.

The abstract statements assume only the reflection identity, and so apply to any extension however obtained. The concrete ones are about the explicit witness TauCeti.lineSchwarzReflection 0 1 q b f of the reflection principle across the real axis with an arbitrary target line; its holomorphy and its agreement with f on the closed upper half-plane are TauCeti.differentiableOn_lineSchwarzReflection_of_symmetric and TauCeti.lineSchwarzReflection_of_coord_im_nonneg.

Main results

• TauCeti.deriv_conj_eq_mul_conj_deriv and TauCeti.deriv_deriv_conj_eq_mul_conj_deriv_deriv -- the first and second derivatives of a function intertwining conjugation with an affine reflection satisfy the same intertwining relation, with the additive constant gone.
• TauCeti.logDeriv_deriv_conj_eq_conj_logDeriv_deriv -- the pre-Schwarzian derivative intertwines conjugation with conjugation.
• TauCeti.im_logDeriv_deriv_eq_zero -- so it is real on the real axis.
• TauCeti.im_div_deriv_lineSchwarzReflection_eq_zero -- on the real axis the derivative of the reflected extension is a real multiple of the direction of the target line.
• TauCeti.im_logDeriv_deriv_lineSchwarzReflection_eq_zero -- the pre-Schwarzian derivative of the reflected extension is real on the real axis.
• TauCeti.eqOn_logDeriv_deriv_lineSchwarzReflection -- it extends the pre-Schwarzian derivative of the original branch.
• TauCeti.logDeriv_deriv_lineSchwarzReflection_conj -- it is conjugation-symmetric.
• TauCeti.differentiableOn_logDeriv_deriv_lineSchwarzReflection -- for an injective branch mapping the upper half-plane to one side of the target line, it is holomorphic across the axis.
• TauCeti.exists_differentiableOn_eqOn_logDeriv_deriv -- the pre-Schwarzian derivative of a map of the upper half-plane with straight boundary arcs away from a set S continues to a conjugation-symmetric function holomorphic away from the real points of S.

References

• L. Ahlfors, Complex Analysis, Ch. 6, Section 2.
• T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Ch. 2.

theorem TauCeti.deriv_conj_eq_mul_conj_deriv {Ω : Set ℂ} {F : ℂ → ℂ} {c u : ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hrefl : ∀ z ∈ Ω, F ((starRingEnd ℂ) z) = c + u * (starRingEnd ℂ) (F z)) {z : ℂ} (hz : z ∈ Ω) : deriv F ((starRingEnd ℂ) z) = u * (starRingEnd ℂ) (deriv F z)

The derivative inherits an affine reflection identity, without its constant. If F carries conjugation to the affine reflection w ↦ c + u * conj w on a conjugation-symmetric open set, then deriv F carries conjugation to w ↦ u * conj w. No differentiability is assumed: the identity also holds, with both sides 0, wherever F fails to be differentiable.

theorem TauCeti.deriv_deriv_conj_eq_mul_conj_deriv_deriv {Ω : Set ℂ} {F : ℂ → ℂ} {c u : ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hrefl : ∀ z ∈ Ω, F ((starRingEnd ℂ) z) = c + u * (starRingEnd ℂ) (F z)) {z : ℂ} (hz : z ∈ Ω) : deriv (deriv F) ((starRingEnd ℂ) z) = u * (starRingEnd ℂ) (deriv (deriv F) z)

The second derivative inherits the same reflection identity. If F intertwines conjugation with an affine reflection on a conjugation-symmetric open set, then its second derivative obeys the same multiplier relation as its first derivative.

theorem TauCeti.logDeriv_deriv_conj_eq_conj_logDeriv_deriv {Ω : Set ℂ} {F : ℂ → ℂ} {c u : ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hrefl : ∀ z ∈ Ω, F ((starRingEnd ℂ) z) = c + u * (starRingEnd ℂ) (F z)) {z : ℂ} (hz : z ∈ Ω) : logDeriv (deriv F) ((starRingEnd ℂ) z) = (starRingEnd ℂ) (logDeriv (deriv F) z)

The pre-Schwarzian derivative of a reflection-symmetric function is conjugation-symmetric. The factor u of the target reflection cancels between the second derivative and the first, so logDeriv (deriv F) = deriv (deriv F) / deriv F intertwines conjugation with conjugation, whatever the target line was. The degenerate factor u = 0 is allowed: there F is constant on Ω and both sides vanish.

theorem TauCeti.im_logDeriv_deriv_eq_zero {Ω : Set ℂ} {F : ℂ → ℂ} {c u : ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hrefl : ∀ z ∈ Ω, F ((starRingEnd ℂ) z) = c + u * (starRingEnd ℂ) (F z)) {x : ℂ} (hx : x ∈ Ω) (hx0 : x.im = 0) : (logDeriv (deriv F) x).im = 0

The pre-Schwarzian derivative of a reflection-symmetric function is real on the real axis.

theorem TauCeti.im_div_deriv_lineSchwarzReflection_eq_zero {Ω : Set ℂ} {f : ℂ → ℂ} {q b : ℂ} (hb : b ≠ 0) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hline : ∀ z ∈ Ω, z.im = 0 → ((f z - q) / b).im = 0) {x : ℂ} (hx : x ∈ Ω) (hx0 : x.im = 0) : (deriv (lineSchwarzReflection 0 1 q b f) x / b).im = 0

On the real axis the reflected extension moves along the target line. For boundary values on the line through q with direction b, the derivative of the extension at a real point is a real multiple of b.

theorem TauCeti.im_logDeriv_deriv_lineSchwarzReflection_eq_zero {Ω : Set ℂ} {f : ℂ → ℂ} {q b : ℂ} (hb : b ≠ 0) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hline : ∀ z ∈ Ω, z.im = 0 → ((f z - q) / b).im = 0) {x : ℂ} (hx : x ∈ Ω) (hx0 : x.im = 0) : (logDeriv (deriv (lineSchwarzReflection 0 1 q b f)) x).im = 0

The pre-Schwarzian derivative of the reflected extension is real on the real axis. The hypotheses are those of the reflection principle across the real axis: the domain is symmetric, and the boundary values of f lie on the line through q with direction b.

theorem TauCeti.eqOn_logDeriv_deriv_lineSchwarzReflection {f : ℂ → ℂ} {q b : ℂ} (hb : b ≠ 0) : Set.EqOn (logDeriv (deriv (lineSchwarzReflection 0 1 q b f))) (logDeriv (deriv f)) {z : ℂ | 0 < z.im}

The reflected extension has the same pre-Schwarzian derivative as the original branch. On the open upper half-plane the extension agrees with f, hence so do all their derivatives.

theorem TauCeti.logDeriv_deriv_lineSchwarzReflection_conj {Ω : Set ℂ} {f : ℂ → ℂ} {q b : ℂ} (hb : b ≠ 0) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hline : ∀ z ∈ Ω, z.im = 0 → ((f z - q) / b).im = 0) {z : ℂ} (hz : z ∈ Ω) : logDeriv (deriv (lineSchwarzReflection 0 1 q b f)) ((starRingEnd ℂ) z) = (starRingEnd ℂ) (logDeriv (deriv (lineSchwarzReflection 0 1 q b f)) z)

The pre-Schwarzian derivative of the reflected extension is conjugation-symmetric. For boundary values on the line through q with direction b, the pre-Schwarzian derivative of the extension intertwines conjugation with conjugation on the symmetric domain.

theorem TauCeti.differentiableOn_logDeriv_deriv_lineSchwarzReflection {Ω : Set ℂ} {f : ℂ → ℂ} {q b : ℂ} (hb : b ≠ 0) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hline : ∀ z ∈ Ω, z.im = 0 → ((f z - q) / b).im = 0) (hside : ∀ z ∈ Ω, 0 < z.im → 0 < ((f z - q) / b).im) (hinj : Set.InjOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) : DifferentiableOn ℂ (logDeriv (deriv (lineSchwarzReflection 0 1 q b f))) Ω

The pre-Schwarzian derivative of a reflected conformal map is holomorphic across the axis. Let f be continuous and injective on the closed upper part of a conjugation-symmetric open set Ω and holomorphic on its open upper part, with boundary values on the line through q with direction b and with the open upper part mapped strictly to the left of that line. Then the reflected extension is injective with nonvanishing derivative on Ω, so its pre-Schwarzian derivative is holomorphic on all of Ω, the real points included.

theorem TauCeti.exists_differentiableOn_eqOn_logDeriv_deriv {f : ℂ → ℂ} {S : Set ℂ} (hholo : DifferentiableOn ℂ f {z : ℂ | 0 < z.im}) (hderiv : ∀ (z : ℂ), 0 < z.im → deriv f z ≠ 0) (hloc : ∀ (x : ℝ), ↑x ∉ S → ∃ r > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ContinuousOn f (Metric.ball (↑x) r ∩ {z : ℂ | 0 ≤ z.im}) ∧ Set.InjOn f (Metric.ball (↑x) r ∩ {z : ℂ | 0 ≤ z.im}) ∧ (∀ z ∈ Metric.ball (↑x) r, z.im = 0 → ((f z - q) / b).im = 0) ∧ ∀ z ∈ Metric.ball (↑x) r, 0 < z.im → 0 < ((f z - q) / b).im) : ∃ (φ : ℂ → ℂ), DifferentiableOn ℂ φ (S ∩ {z : ℂ | z.im = 0})ᶜ ∧ Set.EqOn φ (logDeriv (deriv f)) {z : ℂ | 0 < z.im} ∧ ∀ (z : ℂ), φ ((starRingEnd ℂ) z) = (starRingEnd ℂ) (φ z)

The pre-Schwarzian derivative continues across straight boundary arcs. Let f be holomorphic with nonvanishing derivative on the open upper half-plane, and suppose that near every real point outside S it extends continuously and injectively to the real axis, with boundary values on a line and the nearby upper half-plane mapped strictly to one side of that line. Then the pre-Schwarzian derivative logDeriv (deriv f) continues to a function holomorphic away from the real points of S and symmetric under conjugation.

This is the situation of a conformal map of the upper half-plane onto a polygon, with S the set of prevertices: each boundary interval between consecutive prevertices is carried into one side of the polygon. The continuation is in fact holomorphic at every non-real point; the theorem permits exceptions only at the real points of S.