The Cayley transform of the closed upper half-plane

The Cayley transform z ↦ (z - i) / (z + i) carries the open upper half-plane bijectively onto the open unit disc, and the closed upper half-plane {z | 0 ≤ z.im} bijectively onto the closed unit disc with the point 1 removed; the missing point 1 is the limit of the transform at infinity.

This file records these facts for the transform as a map ℂ → ℂ, so that a statement about maps continuous on the closed unit disc and holomorphic inside it can be transported to the closed upper half-plane. The open-half-plane restriction, centred at an arbitrary point of ℍ, is UpperHalfPlane.discCoordinate.

Main statements

• TauCeti.norm_sub_I_div_add_I_le_one_iff and TauCeti.norm_sub_I_div_add_I_lt_one_iff: the transform lands in the closed (open) unit disc exactly at points of the closed (open) upper half-plane.
• TauCeti.injOn_sub_I_div_add_I: the transform is injective off its pole -i.
• TauCeti.sub_I_div_add_I_sub_sub_I_div_add_I: the difference of two values of the transform.
• TauCeti.continuousAt_sub_I_div_add_I and TauCeti.norm_sub_I_div_norm_add_I_ofReal: continuity and unit norm at real boundary points.
• TauCeti.one_sub_conj_mul_sub_I_div_add_I_ne_zero: the denominator of a standard disc automorphism does not vanish at a real boundary point in Cayley coordinates.
• TauCeti.bijOn_sub_I_div_add_I_upperHalfPlaneSet: the transform is a bijection from the open upper half-plane onto the open unit disc.
• TauCeti.bijOn_I_mul_one_add_div_one_sub_ball: its inverse w ↦ i (1 + w) / (1 - w) is a bijection from the open unit disc onto the open upper half-plane.
• TauCeti.bijOn_sub_I_div_add_I_im_nonneg: the transform is a bijection from the closed upper half-plane onto the closed unit disc minus 1.
• TauCeti.differentiableOn_sub_I_div_add_I: the transform is holomorphic away from its pole.
• TauCeti.differentiableOn_sub_I_div_add_I_im_nonneg: in particular, it is holomorphic on a neighbourhood of the closed upper half-plane.
• TauCeti.hasDerivAt_I_mul_one_add_div_one_sub: the derivative of the inverse transform.
• TauCeti.logDeriv_deriv_I_mul_one_add_div_one_sub: its pre-Schwarzian.
• TauCeti.cayley_simple_fraction: transport of a real-boundary simple fraction.
• TauCeti.I_mul_one_add_sub_I_div_add_I_div_one_sub: the inverse identity.
• TauCeti.boundaryCayley: the boundary Cayley map from ℝ to Circle.
• TauCeti.tendsto_sub_I_div_add_I_cobounded: the transform tends to 1 at infinity.

References

• L. V. Ahlfors, Complex Analysis, 3rd ed., McGraw–Hill, 1979, Ch. 3 §3.

theorem TauCeti.add_I_ne_zero_of_im_nonneg {z : ℂ} (hz : 0 ≤ z.im) : z + Complex.I ≠ 0

The denominator of the Cayley transform does not vanish on the closed upper half-plane.

theorem TauCeti.norm_sub_I_div_add_I_le_one_iff {z : ℂ} (hz : z + Complex.I ≠ 0) : ‖(z - Complex.I) / (z + Complex.I)‖ ≤ 1 ↔ 0 ≤ z.im

The Cayley transform lies in the closed unit disc exactly on the closed upper half-plane.

theorem TauCeti.norm_sub_I_div_add_I_lt_one_iff {z : ℂ} (hz : z + Complex.I ≠ 0) : ‖(z - Complex.I) / (z + Complex.I)‖ < 1 ↔ 0 < z.im

The Cayley transform lies in the open unit disc exactly on the open upper half-plane.

theorem TauCeti.continuousAt_sub_I_div_add_I (x : ℝ) : ContinuousAt (fun (z : ℂ) => (z - Complex.I) / (z + Complex.I)) ↑x

The Cayley transform is continuous at every real point.

@[simp]

theorem TauCeti.norm_sub_I_div_norm_add_I_ofReal (x : ℝ) : ‖↑x - Complex.I‖ / ‖↑x + Complex.I‖ = 1

The Cayley transform of a real point lies on the unit circle.

theorem TauCeti.one_sub_conj_mul_sub_I_div_add_I_ne_zero (c : Complex.UnitDisc) (x : ℝ) : 1 - (starRingEnd ℂ) ↑c * ((↑x - Complex.I) / (↑x + Complex.I)) ≠ 0

The denominator of a standard disc automorphism does not vanish at the Cayley transform of a real point.

@[simp]

theorem TauCeti.norm_sub_I_div_norm_add_I_le_one_iff {z : ℂ} (hz : z + Complex.I ≠ 0) : ‖z - Complex.I‖ / ‖z + Complex.I‖ ≤ 1 ↔ 0 ≤ z.im

The closed-disc criterion in the normal form used by simp after norm_div.

@[simp]

theorem TauCeti.norm_sub_I_div_norm_add_I_lt_one_iff {z : ℂ} (hz : z + Complex.I ≠ 0) : ‖z - Complex.I‖ / ‖z + Complex.I‖ < 1 ↔ 0 < z.im

The open-disc criterion in the normal form used by simp after norm_div.

theorem TauCeti.injOn_sub_I_div_add_I : Set.InjOn (fun (z : ℂ) => (z - Complex.I) / (z + Complex.I)) {z : ℂ | z + Complex.I ≠ 0}

The Cayley transform is injective wherever its denominator does not vanish.

theorem TauCeti.sub_I_div_add_I_sub_sub_I_div_add_I {s t : ℂ} (hs : s + Complex.I ≠ 0) (ht : t + Complex.I ≠ 0) : (s - Complex.I) / (s + Complex.I) - (t - Complex.I) / (t + Complex.I) = 2 * Complex.I * (s - t) / ((s + Complex.I) * (t + Complex.I))

The Cayley transform has the difference quotient 2 * i / ((s + i) * (t + i)).

theorem TauCeti.I_mul_one_add_sub_I_div_add_I_div_one_sub {z : ℂ} (hz : z + Complex.I ≠ 0) : Complex.I * (1 + (z - Complex.I) / (z + Complex.I)) / (1 - (z - Complex.I) / (z + Complex.I)) = z

The inverse Cayley transform takes the Cayley image of a point back to that point.

theorem TauCeti.bijOn_sub_I_div_add_I_upperHalfPlaneSet : Set.BijOn (fun (z : ℂ) => (z - Complex.I) / (z + Complex.I)) UpperHalfPlane.upperHalfPlaneSet (Metric.ball 0 1)

The Cayley transform of the open upper half-plane. The map z ↦ (z - i) / (z + i) is a bijection from the open upper half-plane onto the open unit disc.

theorem TauCeti.bijOn_I_mul_one_add_div_one_sub_ball : Set.BijOn (fun (w : ℂ) => Complex.I * (1 + w) / (1 - w)) (Metric.ball 0 1) UpperHalfPlane.upperHalfPlaneSet

The inverse Cayley transform. The map w ↦ i (1 + w) / (1 - w) is a bijection from the open unit disc onto the open upper half-plane; it inverts z ↦ (z - i) / (z + i).

theorem TauCeti.bijOn_sub_I_div_add_I_im_nonneg : Set.BijOn (fun (z : ℂ) => (z - Complex.I) / (z + Complex.I)) {z : ℂ | 0 ≤ z.im} (Metric.closedBall 0 1 \ {1})

The Cayley transform of the closed upper half-plane. The map z ↦ (z - i) / (z + i) is a bijection from the closed upper half-plane onto the closed unit disc with the point 1 removed.

theorem TauCeti.differentiableOn_sub_I_div_add_I : DifferentiableOn ℂ (fun (z : ℂ) => (z - Complex.I) / (z + Complex.I)) {z : ℂ | z + Complex.I ≠ 0}

The Cayley transform is complex differentiable away from its pole at -i.

theorem TauCeti.differentiableOn_sub_I_div_add_I_im_nonneg : DifferentiableOn ℂ (fun (z : ℂ) => (z - Complex.I) / (z + Complex.I)) {z : ℂ | 0 ≤ z.im}

The Cayley transform is complex differentiable at every point of the closed upper half-plane.

theorem TauCeti.hasDerivAt_I_mul_one_add_div_one_sub {w : ℂ} (hw : w ≠ 1) : HasDerivAt (fun (u : ℂ) => Complex.I * (1 + u) / (1 - u)) (2 * Complex.I / (1 - w) ^ 2) w

The derivative of the inverse Cayley transform w ↦ i (1 + w) / (1 - w) away from its pole at 1 is 2 i / (1 - w) ^ 2.

theorem TauCeti.logDeriv_deriv_I_mul_one_add_div_one_sub {ζ : ℂ} (hζ : ζ ≠ 1) : logDeriv (deriv fun (ξ : ℂ) => Complex.I * (1 + ξ) / (1 - ξ)) ζ = 2 / (1 - ζ)

The pre-Schwarzian of the inverse Cayley transform is 2 / (1 - ζ).

theorem TauCeti.tendsto_sub_I_div_add_I_cobounded : Filter.Tendsto (fun (z : ℂ) => (z - Complex.I) / (z + Complex.I)) (Bornology.cobounded ℂ) (nhds 1)

The Cayley transform tends to 1 at infinity: the point 1 it omits from the closed disc is the image of ∞.

theorem TauCeti.tendsto_I_mul_one_add_div_one_sub_nhdsWithin_one : Filter.Tendsto (fun (ζ : ℂ) => Complex.I * (1 + ζ) / (1 - ζ)) (nhdsWithin 1 (Metric.ball 0 1)) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet)

The inverse Cayley transform tends to infinity within the upper half-plane as the disc variable tends to the omitted boundary point 1.

noncomputable def TauCeti.boundaryCayley (x : ℝ) : Circle

The boundary Cayley map from the real line to the unit circle, sending x to (x - i) / (x + i).

Equations

• TauCeti.boundaryCayley x = ⟨(↑x - Complex.I) / (↑x + Complex.I), ⋯⟩

@[simp]

theorem TauCeti.coe_boundaryCayley (x : ℝ) : ↑(boundaryCayley x) = (↑x - Complex.I) / (↑x + Complex.I)

The boundary Cayley map as a complex-valued formula.

@[simp]

theorem TauCeti.boundaryCayley_ne_one (x : ℝ) : boundaryCayley x ≠ 1

The boundary Cayley map never takes the omitted value 1.

theorem TauCeti.cayley_simple_fraction {ζ : ℂ} (x : ℝ) (hζ1 : ζ ≠ 1) (hζx : ζ ≠ (↑x - Complex.I) / (↑x + Complex.I)) : 1 / (Complex.I * (1 + ζ) / (1 - ζ) - ↑x) * (2 * Complex.I / (1 - ζ) ^ 2) = 1 / (ζ - (↑x - Complex.I) / (↑x + Complex.I)) + 1 / (1 - ζ)

Under the inverse Cayley transform c, the simple fraction c' / (c - x) at a real point x splits into the simple fraction at its Cayley image and one at 1.