Conformal maps of the upper half-plane onto polygonal domains

A polygonal domain is described here by its local geometry at its boundary points: near a boundary point w that is not a vertex the domain U coincides with an open half-plane {z | 0 < ((z - q) / b).im}, and near the vertex v i it coincides with the open sector of opening (e i + 1) * π at v i. Both convex and reentrant vertices are allowed.

Let f be a holomorphic bijection of the upper half-plane onto such a domain U that extends to a continuous injection of the closed upper half-plane, with prevertices f (a i) = v i, and that tends at infinity to a boundary point p of U which is not a vertex and is not a boundary value of f. These are the properties that Carathéodory's boundary correspondence supplies for a Riemann map of a polygon, once it is transported to the upper half-plane with infinity sent to a boundary point that is not a vertex; that transport is not carried out here.

An unbounded polygonal domain has, besides finitely many vertices, a vertex at infinity: far from some point c it coincides with the open sector {|arg ((z - c) / b)| < β * π / 2} of opening β * π, where 0 < β < 2, so that its two unbounded sides lie on lines through c. For such a domain the map f is instead required to tend to infinity at infinity, so that the point at infinity of the half-plane is the prevertex of the vertex at infinity. The vertex at infinity may also have opening 0: far from c the domain coincides with the open half-strip {0 < re ((z - c) / b), 0 < im ((z - c) / b) < π}, whose two unbounded sides are parallel rays. It may also have opening 2: far from c the domain coincides with the exterior of the closed half-strip {0 ≤ re ((z - c) / b), 0 ≤ im ((z - c) / b) ≤ π}, so that its two parallel unbounded sides point the same way and the domain surrounds the half-strip between them. That a Riemann map of such a domain has these properties is not established here.

This file derives from these global conditions the local side and corner conditions of TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_boundary, together with the limit of z * f''(z) / f'(z) at infinity, which is -2 in the bounded case, β - 1 for a sector at infinity, -1 for a half-strip, and 1 for the exterior of a half-strip, and so proves that such an f is an affine image of the normalized Schwarz--Christoffel primitive for the prevertices a i and the turning exponents e i. The only geometric input is local: a boundary value of f lies on the frontier of U, and near a side or a vertex, or far out along an unbounded side, that frontier lies on the bounding line or on the two bounding rays.

Main results

• TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_domain -- a conformal map of the upper half-plane onto a polygonal domain, continuous and injective up to the real axis and tending to a side at infinity, is an affine image of the Schwarz--Christoffel primitive.
• TauCeti.exponent_sum_eq_neg_two_of_polygonal_domain -- the turning exponents of such a polygonal domain sum to -2: its interior angles sum to (n - 2) * π.
• TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_unbounded_polygonal_domain -- a conformal map of the upper half-plane onto an unbounded polygonal domain, continuous and injective up to the real axis and tending to infinity at infinity, is an affine image of the Schwarz--Christoffel primitive.
• TauCeti.exponent_sum_eq_sub_one_of_unbounded_polygonal_domain -- the turning exponents of the finite vertices of such a domain sum to β - 1.
• TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStrip_polygonal_domain and TauCeti.exponent_sum_eq_neg_one_of_halfStrip_polygonal_domain -- the same for a polygonal domain with a half-strip end, whose finite turning exponents sum to -1.
• TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStripExterior_polygonal_domain and TauCeti.exponent_sum_eq_one_of_halfStripExterior_polygonal_domain -- the same for a polygonal domain whose end is the exterior of a half-strip, whose finite turning exponents sum to 1.

References

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

Boundary values of a conformal map onto U

The Schwarz--Christoffel formula

theorem TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_domain {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {v : ι → ℂ} {p : ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (nhds p)) (hpf : p ∉ f '' {z : ℂ | 0 ≤ z.im}) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) : Set.EqOn f (fun (z : ℂ) => deriv f ↑z₀ / schwarzChristoffelIntegrand a e ↑z₀ * schwarzChristoffelPrimitive a e z₀ z + f ↑z₀) UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel formula for a conformal map onto a polygonal domain. Let U coincide near each boundary point that is not a vertex with an open half-plane, and near the vertex v i with the open sector of opening (e i + 1) * π at v i. Let f be holomorphic on the upper half-plane, map it onto U, and extend to a continuous injection of the closed upper half-plane with f (a i) = v i; suppose also that f z tends at infinity to a point p which is not a value of f on the closed upper half-plane. Then throughout the upper half-plane

f z = (f'(z₀) / integrand(z₀)) * F z + f z₀,

where F is the normalized Schwarz--Christoffel primitive for the prevertices a and the turning exponents e.

theorem TauCeti.exponent_sum_eq_neg_two_of_polygonal_domain {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {v : ι → ℂ} {p : ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (nhds p)) (hpf : p ∉ f '' {z : ℂ | 0 ≤ z.im}) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) : ∑ i : ι, e i = -2

The angle sum of a polygonal domain. Under the hypotheses of TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_domain, the turning exponents sum to -2. Equivalently, the interior angles (e i + 1) * π of the polygon sum to (n - 2) * π, where n is the number of vertices.

theorem TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_unbounded_polygonal_domain {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {v : ι → ℂ} {β : ℝ} (hβ : β ∈ Set.Ioo 0 2) (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (Bornology.cobounded ℂ)) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) (hinfty : ∃ (ρ : ℝ) (c : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ |((z - c) / b).arg| < β * Real.pi / 2)) : Set.EqOn f (fun (z : ℂ) => deriv f ↑z₀ / schwarzChristoffelIntegrand a e ↑z₀ * schwarzChristoffelPrimitive a e z₀ z + f ↑z₀) UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel formula for a conformal map onto an unbounded polygonal domain. Let U coincide near each boundary point that is not a vertex with an open half-plane, near the vertex v i with the open sector of opening (e i + 1) * π at v i, and far from a point c with the open sector {|arg ((z - c) / b)| < β * π / 2} of opening β * π, where 0 < β < 2: so U has, besides the finite vertices, a vertex at infinity between two unbounded sides on lines through c. Let f be holomorphic on the upper half-plane, map it onto U, and extend to a continuous injection of the closed upper half-plane with f (a i) = v i; suppose also that f z tends to infinity at infinity. Then throughout the upper half-plane

f z = (f'(z₀) / integrand(z₀)) * F z + f z₀,

where F is the normalized Schwarz--Christoffel primitive for the prevertices a and the turning exponents e.

theorem TauCeti.exponent_sum_eq_sub_one_of_unbounded_polygonal_domain {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {v : ι → ℂ} {β : ℝ} (hβ : β ∈ Set.Ioo 0 2) (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (Bornology.cobounded ℂ)) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) (hinfty : ∃ (ρ : ℝ) (c : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ |((z - c) / b).arg| < β * Real.pi / 2)) : ∑ i : ι, e i = β - 1

The angle sum of an unbounded polygonal domain. Under the hypotheses of TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_unbounded_polygonal_domain, the turning exponents of the finite vertices sum to β - 1. Equivalently, the finite vertices of the polygon, of interior angles (e i + 1) * π, together with the vertex at infinity of opening β * π, have interior angles summing to (n - 2) * π when the vertex at infinity is assigned the angle -β * π, where n is the number of vertices including the one at infinity.

theorem TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStrip_polygonal_domain {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {v : ι → ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (Bornology.cobounded ℂ)) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) (hinfty : ∃ (ρ : ℝ) (c : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ 0 < ((z - c) / b).re ∧ ((z - c) / b).im ∈ Set.Ioo 0 Real.pi)) : Set.EqOn f (fun (z : ℂ) => deriv f ↑z₀ / schwarzChristoffelIntegrand a e ↑z₀ * schwarzChristoffelPrimitive a e z₀ z + f ↑z₀) UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel formula for a conformal map onto a polygonal domain with a half-strip end. Let U coincide near each boundary point that is not a vertex with an open half-plane, near the vertex v i with the open sector of opening (e i + 1) * π at v i, and far from a point c with the open half-strip {0 < re ((z - c) / b), 0 < im ((z - c) / b) < π}: so U has, besides the finite vertices, a vertex at infinity of opening 0 between two parallel unbounded sides. Let f be holomorphic on the upper half-plane, map it onto U, and extend to a continuous injection of the closed upper half-plane with f (a i) = v i; suppose also that f z tends to infinity at infinity. Then throughout the upper half-plane

f z = (f'(z₀) / integrand(z₀)) * F z + f z₀,

where F is the normalized Schwarz--Christoffel primitive for the prevertices a and the turning exponents e.

theorem TauCeti.exponent_sum_eq_neg_one_of_halfStrip_polygonal_domain {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {v : ι → ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (Bornology.cobounded ℂ)) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) (hinfty : ∃ (ρ : ℝ) (c : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ 0 < ((z - c) / b).re ∧ ((z - c) / b).im ∈ Set.Ioo 0 Real.pi)) : ∑ i : ι, e i = -1

The angle sum of a polygonal domain with a half-strip end. Under the hypotheses of TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStrip_polygonal_domain, the turning exponents of the finite vertices sum to -1: this is the opening β = 0 case of TauCeti.exponent_sum_eq_sub_one_of_unbounded_polygonal_domain.

theorem TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStripExterior_polygonal_domain {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {v : ι → ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (Bornology.cobounded ℂ)) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) (hinfty : ∃ (ρ : ℝ) (c : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ ((z - c) / b).re < 0 ∨ ((z - c) / b).im ∉ Set.Icc 0 Real.pi)) : Set.EqOn f (fun (z : ℂ) => deriv f ↑z₀ / schwarzChristoffelIntegrand a e ↑z₀ * schwarzChristoffelPrimitive a e z₀ z + f ↑z₀) UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel formula for a conformal map onto a polygonal domain whose end is the exterior of a half-strip. Let U coincide near each boundary point that is not a vertex with an open half-plane, near the vertex v i with the open sector of opening (e i + 1) * π at v i, and far from a point c with the exterior of the closed half-strip {0 ≤ re ((z - c) / b), 0 ≤ im ((z - c) / b) ≤ π}: so U has, besides the finite vertices, a vertex at infinity of opening 2 * π between two parallel unbounded sides pointing the same way. Let f be holomorphic on the upper half-plane, map it onto U, and extend to a continuous injection of the closed upper half-plane with f (a i) = v i; suppose also that f z tends to infinity at infinity. Then throughout the upper half-plane

f z = (f'(z₀) / integrand(z₀)) * F z + f z₀,

where F is the normalized Schwarz--Christoffel primitive for the prevertices a and the turning exponents e.

theorem TauCeti.exponent_sum_eq_one_of_halfStripExterior_polygonal_domain {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {v : ι → ℂ} (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i) (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (Bornology.cobounded ℂ)) (hside : ∀ w ∈ frontier U, (∀ (i : ι), w ≠ v i) → ∃ ρ > 0, ∃ (q : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im) (hcorner : ∀ (i : ι), ∃ ρ > 0, ∃ (b : ℂ), b ≠ 0 ∧ ∀ z ∈ Metric.ball (v i) ρ, z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) (hinfty : ∃ (ρ : ℝ) (c : ℂ) (b : ℂ), b ≠ 0 ∧ ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ ((z - c) / b).re < 0 ∨ ((z - c) / b).im ∉ Set.Icc 0 Real.pi)) : ∑ i : ι, e i = 1

The angle sum of a polygonal domain whose end is the exterior of a half-strip. Under the hypotheses of TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStripExterior_polygonal_domain, the turning exponents of the finite vertices sum to 1: this is the opening β = 2 case of TauCeti.exponent_sum_eq_sub_one_of_unbounded_polygonal_domain.