The pre-Schwarzian derivative: composition, rigidity, and asymptotics

The pre-Schwarzian derivative of a holomorphic function f is logDeriv (deriv f) = f'' / f'. Postcomposing f with w ↦ a * w + b for a ≠ 0 leaves it unchanged, and this file proves the converse: on a domain -- an open preconnected subset of ℂ -- two holomorphic functions with nonvanishing derivatives and the same pre-Schwarzian derivative differ by exactly such a postcomposition. That is the statement which integrates a pre-Schwarzian differential equation, such as the Schwarz--Christoffel equation f'' / f' = ∑ i, e i / (z - a i), back to its solutions.

The second half of the file computes the pre-Schwarzian derivative of a corner power f = w + h ^ β, where h is holomorphic and β is a fixed complex exponent. Its pre-Schwarzian is (β - 1) * logDeriv h + logDeriv (deriv h), independently of the branch, and at a simple zero p of h one has the residue asymptotic (z - p) * logDeriv (deriv f) z → β - 1. So the exponent of a corner power is read off from the residue of the pre-Schwarzian derivative at that corner, which is how a map with a corner of opening α contributes the residue α / π - 1 to the Schwarz--Christoffel partial-fraction identity. The exponent β = 0 is played by a logarithm f of h, exp ∘ f = h: its pre-Schwarzian is logDeriv (deriv h) - logDeriv h, with residue asymptotic -1 at a simple zero of h.

The chain rule describes the effect of changing the source coordinate. In particular, if g is holomorphic near zero with g'(0) ≠ 0, the map f z = g (-1 / z) satisfies z * f''(z) / f'(z) → -2 at infinity. Thus its pre-Schwarzian tends to zero, the decay condition needed to identify a meromorphic pre-Schwarzian by its finite poles and residues.

Main results

• TauCeti.exists_eqOn_const_mul_add_iff_logDeriv_deriv_eqOn -- two holomorphic functions with nonvanishing derivatives on a domain have the same pre-Schwarzian derivative exactly when one is w ↦ a * w + b applied to the other, for some a ≠ 0.
• TauCeti.logDeriv_deriv_of_eqOn_add_cpow -- the pre-Schwarzian derivative of a corner power.
• TauCeti.tendsto_sub_mul_logDeriv_deriv_of_eqOn_add_cpow -- at a simple zero of the base, the pre-Schwarzian derivative of a corner power has residue asymptotic β - 1.
• TauCeti.logDeriv_deriv_of_eqOn_exp and TauCeti.tendsto_sub_mul_logDeriv_deriv_of_eqOn_exp -- the same for a logarithm, with residue asymptotic -1.
• TauCeti.logDeriv_deriv_comp -- the pre-Schwarzian chain rule.
• TauCeti.tendsto_logDeriv_deriv_comp_neg_inv -- decay at infinity for a map regular in the inverse coordinate.
• TauCeti.tendsto_mul_logDeriv_deriv_of_tendsto_mul_logDeriv_deriv_neg_inv -- a residue asymptotic L at 0 in the normalized inverse coordinate gives -L - 2 at infinity.

References

• L. Ahlfors, Complex Analysis, Ch. 6, Section 2.

theorem TauCeti.logDeriv_deriv_comp {f g : ℂ → ℂ} {z : ℂ} (hf : AnalyticAt ℂ f (g z)) (hg : AnalyticAt ℂ g z) (hfn : deriv f (g z) ≠ 0) (hgn : deriv g z ≠ 0) : logDeriv (deriv (f ∘ g)) z = logDeriv (deriv f) (g z) * deriv g z + logDeriv (deriv g) z

The pre-Schwarzian chain rule for locally conformal holomorphic functions.

theorem TauCeti.logDeriv_deriv_comp_neg_inv {g : ℂ → ℂ} {z : ℂ} (hg : AnalyticAt ℂ g (-z⁻¹)) (hgn : deriv g (-z⁻¹) ≠ 0) (hz : z ≠ 0) : logDeriv (deriv fun (w : ℂ) => g (-w⁻¹)) z = logDeriv (deriv g) (-z⁻¹) / z ^ 2 - 2 / z

In the coordinate w = -1 / z, the pre-Schwarzian acquires the term -2 / z.

theorem TauCeti.tendsto_mul_logDeriv_deriv_comp_neg_inv {g : ℂ → ℂ} (hg : AnalyticAt ℂ g 0) (hgn : deriv g 0 ≠ 0) : Filter.Tendsto (fun (z : ℂ) => z * logDeriv (deriv fun (w : ℂ) => g (-w⁻¹)) z) (Bornology.cobounded ℂ) (nhds (-2))

If the inverse coordinate of a map is holomorphic and regular at zero, its pre-Schwarzian has leading term -2 / z at infinity. The limit is through the whole complex plane.

theorem TauCeti.tendsto_logDeriv_deriv_comp_neg_inv {g : ℂ → ℂ} (hg : AnalyticAt ℂ g 0) (hgn : deriv g 0 ≠ 0) : Filter.Tendsto (logDeriv (deriv fun (w : ℂ) => g (-w⁻¹))) (Bornology.cobounded ℂ) (nhds 0)

A map regular in the inverse coordinate has pre-Schwarzian tending to zero at infinity.

theorem TauCeti.tendsto_mul_logDeriv_deriv_of_tendsto_mul_logDeriv_deriv_neg_inv {f : ℂ → ℂ} {c b L : ℂ} {r : ℝ} (hr : 0 < r) (hb : b ≠ 0) (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfn : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, deriv f z ≠ 0) (hL : Filter.Tendsto (fun (w : ℂ) => w * logDeriv (deriv fun (w : ℂ) => (f (-w⁻¹) - c) / b) w) (nhdsWithin 0 (Metric.ball 0 r ∩ UpperHalfPlane.upperHalfPlaneSet)) (nhds L)) : Filter.Tendsto (fun (z : ℂ) => z * logDeriv (deriv f) z) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds (-L - 2))

The pre-Schwarzian chain rule at infinity, as a limit. Read the map f of the upper half-plane in the coordinate w ↦ -1 / w and normalize the target by w ↦ (w - c) / b. If the pre-Schwarzian of the result has the residue asymptotic w * F''(w) / F'(w) → L as w tends to 0 in the upper half of a ball, then z * f''(z) / f'(z) → -L - 2 at infinity.

theorem TauCeti.exists_eqOn_const_mul_add_iff_logDeriv_deriv_eqOn {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩconn : IsPreconnected Ω) {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f Ω) (hg : DifferentiableOn ℂ g Ω) (hfn : ∀ z ∈ Ω, deriv f z ≠ 0) (hgn : ∀ z ∈ Ω, deriv g z ≠ 0) : (∃ (a : ℂ), a ≠ 0 ∧ ∃ (b : ℂ), Set.EqOn f (fun (z : ℂ) => a * g z + b) Ω) ↔ Set.EqOn (logDeriv (deriv f)) (logDeriv (deriv g)) Ω

Rigidity of the pre-Schwarzian derivative. Two holomorphic functions with nonvanishing derivatives on a domain have equal pre-Schwarzian derivatives exactly when one is obtained from the other by postcomposition with w ↦ a * w + b for a nonzero constant a.

theorem TauCeti.logDeriv_deriv_of_eqOn_add_cpow {h f : ℂ → ℂ} {s : Set ℂ} {w β : ℂ} (hs : IsOpen s) (hh : DifferentiableOn ℂ h s) (hslit : ∀ z ∈ s, h z ∈ Complex.slitPlane) (hβ : β ≠ 0) (hf : Set.EqOn f (fun (z : ℂ) => w + h z ^ β) s) {z : ℂ} (hz : z ∈ s) (hdh : deriv h z ≠ 0) : logDeriv (deriv f) z = (β - 1) * logDeriv h z + logDeriv (deriv h) z

The pre-Schwarzian derivative of a corner power. Where f agrees with w + h ^ β on an open set on which the holomorphic base h avoids the branch cut, the pre-Schwarzian derivative of f is (β - 1) * logDeriv h + logDeriv (deriv h). The branch used to define the power leaves no trace.

theorem TauCeti.tendsto_sub_mul_logDeriv_deriv_of_eqOn_add_cpow {h f : ℂ → ℂ} {s : Set ℂ} {p w β : ℂ} {U : Set ℂ} (hU : IsOpen U) (hpU : p ∈ U) (hh : DifferentiableOn ℂ h U) (hhp : h p = 0) (hdh : deriv h p ≠ 0) (hs : IsOpen s) (_hne : (nhdsWithin p s).NeBot) (hsU : s ⊆ U) (hslit : ∀ z ∈ s, h z ∈ Complex.slitPlane) (hβ : β ≠ 0) (hf : Set.EqOn f (fun (z : ℂ) => w + h z ^ β) s) : Filter.Tendsto (fun (z : ℂ) => (z - p) * logDeriv (deriv f) z) (nhdsWithin p s) (nhds (β - 1))

The residue asymptotic of the pre-Schwarzian derivative at a corner. If the holomorphic base h has a simple zero at p and f agrees with w + h ^ β on an open set s avoiding the branch cut, and s nontrivially approaches p, then (z - p) * logDeriv (deriv f) z tends to β - 1 as z tends to p inside s. The exponent β is thus the residue of the pre-Schwarzian derivative at the corner, shifted by one.

theorem TauCeti.logDeriv_deriv_of_eqOn_exp {h f : ℂ → ℂ} {s : Set ℂ} (hs : IsOpen s) (hf : DifferentiableOn ℂ f s) (hexp : Set.EqOn (fun (z : ℂ) => Complex.exp (f z)) h s) {z : ℂ} (hz : z ∈ s) (hdh : deriv h z ≠ 0) : logDeriv (deriv f) z = logDeriv (deriv h) z - logDeriv h z

The pre-Schwarzian derivative of a logarithm. Where the holomorphic function f is a logarithm of h on an open set, exp ∘ f = h, the pre-Schwarzian derivative of f is logDeriv (deriv h) - logDeriv h. This is the exponent β = 0 counterpart of TauCeti.logDeriv_deriv_of_eqOn_add_cpow.

theorem TauCeti.tendsto_sub_mul_logDeriv_deriv_of_eqOn_exp {h f : ℂ → ℂ} {s : Set ℂ} {p : ℂ} (hh : AnalyticAt ℂ h p) (hhp : h p = 0) (hdh : deriv h p ≠ 0) (hs : IsOpen s) (hf : DifferentiableOn ℂ f s) (hexp : Set.EqOn (fun (z : ℂ) => Complex.exp (f z)) h s) : Filter.Tendsto (fun (z : ℂ) => (z - p) * logDeriv (deriv f) z) (nhdsWithin p s) (nhds (-1))

The residue asymptotic of the pre-Schwarzian derivative of a logarithm. If h has a simple zero at p and the holomorphic function f is a logarithm of h on an open set s, then (z - p) * logDeriv (deriv f) z tends to -1 as z tends to p inside s. This is the exponent β = 0 counterpart of TauCeti.tendsto_sub_mul_logDeriv_deriv_of_eqOn_add_cpow: a logarithm opens a straight edge through p into a parallel-sided end at infinity.