The Schwarz--Christoffel theorem for polygonal Jordan domains

Let U be a bounded domain whose frontier is a Jordan curve, and which is polygonal: near each boundary point that is not one of the finitely many vertices v i it coincides with an open half-plane, and near v i with the open sector of opening (e i + 1) * π at v i, where e i ∈ (-1, 1). Then there are distinct real prevertices a i and complex constants A ≠ 0 and B such that A * F + B maps the upper half-plane bijectively onto U, where F is the normalized Schwarz--Christoffel primitive for a and e, and sends each prevertex to its vertex: A * vertex i + B = v i, where vertex i is the limit of F at a i.

The same holds for an unbounded polygonal domain with a vertex at infinity, one which far out coincides with an open sector of opening β * π, 0 < β < 2, or with an open half-strip, and whose frontier together with the point at infinity is a Jordan curve of the Riemann sphere. The point at infinity of the half-plane is then the prevertex of the vertex at infinity.

Main results

• TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_frontier -- a bounded polygonal Jordan domain is the image of the upper half-plane under an affine image of a Schwarz--Christoffel primitive, with the prevertices sent to the vertices.
• TauCeti.exponent_sum_eq_neg_two_of_isJordanCurve_frontier -- the turning exponents of a bounded polygonal Jordan domain sum to -2, so its interior angles sum to (n - 2) * π.
• TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_insert_infty -- the same representation for an unbounded polygonal Jordan domain with a vertex at infinity.
• TauCeti.exponent_sum_eq_sub_one_of_isJordanCurve_insert_infty -- the turning exponents of the finite vertices of such a domain sum to β - 1.
• TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_of_halfStrip and TauCeti.exponent_sum_eq_neg_one_of_isJordanCurve_of_halfStrip -- the same for an unbounded polygonal Jordan domain with a half-strip end, 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.
• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).

theorem TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_frontier {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUb : Bornology.IsBounded U) (hUJ : IsJordanCurve (frontier U)) {v : ι → ℂ} (hv : Function.Injective v) (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)) : ∃ (a : ι → ℝ), Function.Injective a ∧ ∃ (A : ℂ), A ≠ 0 ∧ ∃ (B : ℂ), Set.BijOn (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet U ∧ ∀ (i : ι), A * schwarzChristoffelVertex a e z₀ i + B = v i

The Schwarz--Christoffel theorem for a bounded polygonal Jordan domain. Let U be a bounded, connected open set whose frontier is a Jordan curve. Suppose that U coincides near each frontier point other than the distinct vertices v i with an open half-plane, and near the vertex v i with the open sector of opening (e i + 1) * π at v i, where e i ∈ (-1, 1). Then there are distinct real prevertices a i and constants A ≠ 0 and B such that z ↦ A * F z + B maps the upper half-plane bijectively onto U, where F is the normalized Schwarz--Christoffel primitive for the prevertices a and the turning exponents e, and such that the Schwarz--Christoffel vertex at a i, the limit of F at a i, is sent to v i.

theorem TauCeti.exponent_sum_eq_neg_two_of_isJordanCurve_frontier {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUb : Bornology.IsBounded U) (hUJ : IsJordanCurve (frontier U)) {v : ι → ℂ} (hv : Function.Injective v) (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 bounded polygonal Jordan domain. Under the hypotheses of TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_frontier, the turning exponents sum to -2: the interior angles (e i + 1) * π at the n vertices sum to (n - 2) * π. So the Schwarz--Christoffel data of a polygonal Jordan domain always satisfy the closing condition ∑ i, e i = -2.

theorem TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_insert_infty {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {β : ℝ} (hβ : β ∈ Set.Ioo 0 2) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) {v : ι → ℂ} (hv : Function.Injective v) (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)) : ∃ (a : ι → ℝ), Function.Injective a ∧ ∃ (A : ℂ), A ≠ 0 ∧ ∃ (B : ℂ), Set.BijOn (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet U ∧ ∀ (i : ι), A * schwarzChristoffelVertex a e z₀ i + B = v i

The Schwarz--Christoffel theorem for an unbounded polygonal Jordan domain. Let U be a connected open set whose frontier, together with the point at infinity, is a Jordan curve of the Riemann sphere. Suppose that U coincides near each frontier point other than the distinct vertices v i with an open half-plane, near the vertex v i with the open sector of opening (e i + 1) * π at v i, where e i ∈ (-1, 1), and far from a point c with the open sector {|arg ((z - c) / b)| < β * π / 2} of opening β * π, where 0 < β < 2: so U has a further vertex at infinity. Then there are distinct real prevertices a i and constants A ≠ 0 and B such that z ↦ A * F z + B maps the upper half-plane bijectively onto U, where F is the normalized Schwarz--Christoffel primitive for the prevertices a and the turning exponents e, and such that the Schwarz--Christoffel vertex at a i, the limit of F at a i, is sent to v i. The prevertex of the vertex at infinity is the point at infinity of the half-plane.

theorem TauCeti.exponent_sum_eq_sub_one_of_isJordanCurve_insert_infty {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {β : ℝ} (hβ : β ∈ Set.Ioo 0 2) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) {v : ι → ℂ} (hv : Function.Injective v) (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 Jordan domain. Under the hypotheses of TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_insert_infty, the turning exponents of the finite vertices sum to β - 1, where β * π is the opening of the sector at infinity.

theorem TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_of_halfStrip {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) {v : ι → ℂ} (hv : Function.Injective v) (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)) : ∃ (a : ι → ℝ), Function.Injective a ∧ ∃ (A : ℂ), A ≠ 0 ∧ ∃ (B : ℂ), Set.BijOn (fun (z : ℂ) => A * schwarzChristoffelPrimitive a e z₀ z + B) UpperHalfPlane.upperHalfPlaneSet U ∧ ∀ (i : ι), A * schwarzChristoffelVertex a e z₀ i + B = v i

The Schwarz--Christoffel theorem for a polygonal Jordan domain with a half-strip end. Let U be a connected open set whose frontier, together with the point at infinity, is a Jordan curve of the Riemann sphere. Suppose that U coincides near each frontier point other than the distinct vertices v i with an open half-plane, near the vertex v i with the open sector of opening (e i + 1) * π at v i, where e i ∈ (-1, 1), and far from a point c with the open half-strip {0 < re ((z - c) / b), 0 < im ((z - c) / b) < π}: so U has a further vertex at infinity, between two parallel sides. Then there are distinct real prevertices a i and constants A ≠ 0 and B such that z ↦ A * F z + B maps the upper half-plane bijectively onto U, where F is the normalized Schwarz--Christoffel primitive for the prevertices a and the turning exponents e, and such that the Schwarz--Christoffel vertex at a i, the limit of F at a i, is sent to v i. The prevertex of the vertex at infinity is the point at infinity of the half-plane.

theorem TauCeti.exponent_sum_eq_neg_one_of_isJordanCurve_of_halfStrip {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) {v : ι → ℂ} (hv : Function.Injective v) (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 Jordan domain with a half-strip end. Under the hypotheses of TauCeti.exists_bijOn_const_mul_schwarzChristoffelPrimitive_add_of_isJordanCurve_of_halfStrip, the turning exponents of the finite vertices sum to -1.