Period-one cylindrical coordinates on the punctured disc

The punctured unit disc is a half-cylinder, with longitudinal coordinate s > 0 and angular coordinate in ℝ / ℤ. The coordinate is exp (-2π(s + it)) on real lifts. The construction uses Mathlib's polar homeomorphism homeomorphUnitSphereProd and AddCircle.homeomorphCircle, so the angular coordinate has period one.

noncomputable def TauCeti.Complex.UnitDisc.cylinderRadius : ↑(Set.Ioi 0) ≃ₜ ↑(Set.Ioo 0 1)

Exponential radial coordinate: positive cylinder length corresponds to radius in (0,1). The normalization makes the angular period equal to one.

@[simp]

theorem TauCeti.Complex.UnitDisc.cylinderRadius_apply (s : ↑(Set.Ioi 0)) : ↑(cylinderRadius s) = Real.exp (-(2 * Real.pi) * ↑s)

The radial coordinate is the normalized decreasing exponential.

@[simp]

theorem TauCeti.Complex.UnitDisc.cylinderRadius_symm_apply (r : ↑(Set.Ioo 0 1)) : ↑(cylinderRadius.symm r) = -Real.log ↑r / (2 * Real.pi)

The inverse radial coordinate is normalized negative logarithmic radius.

noncomputable def TauCeti.Complex.UnitDisc.puncturedPolar : ↑(Metric.ball 0 1 \ {0}) ≃ₜ Circle × ↑(Set.Ioo 0 1)

Polar coordinates on the punctured unit disc, with radius constrained to (0,1). This is the restriction of Mathlib's homeomorphUnitSphereProd.

@[simp]

theorem TauCeti.Complex.UnitDisc.puncturedPolar_apply_fst (z : ↑(Metric.ball 0 1 \ {0})) : ↑(puncturedPolar z).1 = ‖↑z‖⁻¹ • ↑z

The direction of the punctured polar coordinate is the normalized complex vector.

@[simp]

theorem TauCeti.Complex.UnitDisc.puncturedPolar_apply_snd (z : ↑(Metric.ball 0 1 \ {0})) : ↑(puncturedPolar z).2 = ‖↑z‖

The radial component of the punctured polar coordinate is its norm.

@[simp]

theorem TauCeti.Complex.UnitDisc.puncturedPolar_symm_apply (p : Circle × ↑(Set.Ioo 0 1)) : ↑(puncturedPolar.symm p) = ↑p.2 • ↑p.1

The inverse polar map multiplies the unit direction by its positive radius.

noncomputable def TauCeti.Complex.UnitDisc.puncturedCylinder : ↑(Set.Ioi 0) × AddCircle 1 ≃ₜ ↑(Metric.ball 0 1 \ {0})

The period-one cylindrical parameterization of the punctured unit disc. Its real lift is exp (-2π(s + it)).

theorem TauCeti.Complex.UnitDisc.puncturedCylinder_symm_apply (z : ↑(Metric.ball 0 1 \ {0})) : puncturedCylinder.symm z = (cylinderRadius.symm (puncturedPolar z).2, -(AddCircle.homeomorphCircle ⋯).symm (puncturedPolar z).1)

The inverse cylindrical coordinates recover logarithmic radius and angular phase.

theorem TauCeti.Complex.UnitDisc.puncturedCylinder_apply (s : ↑(Set.Ioi 0)) (t : AddCircle 1) : ↑(puncturedCylinder (s, t)) = Real.exp (-(2 * Real.pi) * ↑s) • ↑(-t).toCircle

Evaluation of cylindrical coordinates by radius and the period-one angular coordinate.

theorem TauCeti.Complex.UnitDisc.puncturedCylinder_apply_mk (s : ↑(Set.Ioi 0)) (t : ℝ) : ↑(puncturedCylinder (s, ↑t)) = Complex.exp (-(2 * ↑Real.pi) * (↑↑s + ↑t * Complex.I))

On real angular lifts the cylinder coordinate is the holomorphic exponential.