Basic facts about circular parametrizations

The derivative of circleMap c R is continuous (Complex.continuous_deriv_circleMap).

The trace of a circular parametrization over [0,2π] is the sphere, for arbitrary signed radii. Consequently the exponential t ↦ exp (2π i t / L) and its conjugate cover the unit circle over [0, L] (Complex.image_exp_two_pi_I_div_Icc, Complex.image_exp_neg_two_pi_I_div_Icc).

theorem Complex.continuous_deriv_circleMap (c : ℂ) (R : ℝ) : Continuous (deriv (circleMap c R))

The derivative of the circle parametrisation circleMap c R is continuous.

theorem Complex.image_circleMap_uIcc (c : ℂ) (R : ℝ) : circleMap c R '' Set.uIcc 0 (2 * Real.pi) = Metric.sphere c |R|

The full circular trace over [0,2π] is exactly the circle.

theorem Complex.image_exp_two_pi_I_div_Icc {L : ℝ} (hL : 0 < L) : (fun (t : ℝ) => exp (2 * ↑Real.pi * I * ↑t / ↑L)) '' Set.Icc 0 L = Metric.sphere 0 1

One turn of a unit circular exponential, rescaled to the interval [0, L] of positive length L, covers the unit circle, including both endpoints.

theorem Complex.image_exp_neg_two_pi_I_div_Icc {L : ℝ} (hL : 0 < L) : (fun (t : ℝ) => exp (-(2 * ↑Real.pi * I * ↑t / ↑L))) '' Set.Icc 0 L = Metric.sphere 0 1

The conjugate circular exponential t ↦ exp (-(2π i t / L)) also covers the unit circle over [0, L].