Conformal maps of the closed upper half-plane

This file transports a conformal map of the closed unit disc to the closed upper half-plane. The Cayley transform followed by a rotation identifies the closed upper half-plane with the closed disc minus a specified boundary point, so the transported map has that boundary value as its limit at infinity.

Main statements

• TauCeti.bijOn_mul_left_of_norm_eq_one: multiplication by a unit complex number preserves the open unit disc and carries the closed unit disc with 1 removed to the disc with that number removed.
• TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_injOn_closedBall: transport of a continuous injective closed-disc map which is holomorphic on the open disc.

theorem TauCeti.bijOn_mul_left_of_norm_eq_one {ζ : ℂ} (hζ : ‖ζ‖ = 1) : Set.BijOn (fun (x : ℂ) => ζ * x) (Metric.closedBall 0 1 \ {1}) (Metric.closedBall 0 1 \ {ζ}) ∧ Set.BijOn (fun (x : ℂ) => ζ * x) (Metric.ball 0 1) (Metric.ball 0 1)

Multiplication by a unit complex number maps the closed unit disc with 1 removed bijectively onto the closed unit disc with that number removed, and the open unit disc onto itself.

theorem TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_injOn_closedBall {g : ℂ → ℂ} {Ω : Set ℂ} (hgc : ContinuousOn g (Metric.closedBall 0 1)) (hgd : DifferentiableOn ℂ g (Metric.ball 0 1)) (hgi : Set.InjOn g (Metric.closedBall 0 1)) (hgΩ : g '' Metric.ball 0 1 = Ω) {p : ℂ} (hp : p ∈ frontier Ω) : ∃ (f : ℂ → ℂ), ContinuousOn f {z : ℂ | 0 ≤ z.im} ∧ DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet ∧ Set.BijOn f UpperHalfPlane.upperHalfPlaneSet Ω ∧ Set.BijOn f {z : ℂ | 0 ≤ z.im} (closure Ω \ {p}) ∧ Set.BijOn f {z : ℂ | z.im = 0} (frontier Ω \ {p}) ∧ Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (nhds p)

A conformal map of the closed disc can be transported to the closed upper half-plane. Let g be continuous and injective on the closed unit disc and holomorphic on the open disc, with g applied to the open disc equal to Ω, and let p lie in the frontier of Ω. Then precomposing g with a rotated Cayley transform gives a map which is continuous on the closed upper half-plane, holomorphic on the open upper half-plane, and has the stated bijectivity and limit properties.