Circle Parameterizations

Standard circle parameterizations (counterclockwise and clockwise) and their winding number computations.

Main Results

• circleParam — counterclockwise circle: z₀ + r·exp(2πi(t-a)/(b-a))
• circleParam_winding_eq_one — winding number = 1
• circleParamCW — clockwise circle: reversal of circleParam
• circleParamCW_winding_eq_neg_one — winding number = -1

noncomputable def circleParam (z₀ : ℂ) (r a b t : ℝ) : ℂ

Standard circle parameterization: z₀ + r·exp(2πi(t-a)/(b-a)).

Equations

• circleParam z₀ r a b t = z₀ + ↑r * Complex.exp (2 * ↑Real.pi * Complex.I * ((↑t - ↑a) / (↑b - ↑a)))

theorem circleParam_continuous (z₀ : ℂ) (r a b : ℝ) : Continuous (circleParam z₀ r a b)

theorem circleParam_closed (z₀ : ℂ) (r a b : ℝ) (hab : a < b) : circleParam z₀ r a b a = circleParam z₀ r a b b

theorem circleParam_dist (z₀ : ℂ) (r : ℝ) (hr : 0 ≤ r) (a b : ℝ) (_hab : a < b) (t : ℝ) : ‖circleParam z₀ r a b t - z₀‖ = r

theorem circleParam_deriv (z₀ : ℂ) (r a b : ℝ) (_hab : a < b) (t : ℝ) : deriv (circleParam z₀ r a b) t = ↑r * (2 * ↑Real.pi * Complex.I / (↑b - ↑a)) * Complex.exp (2 * ↑Real.pi * Complex.I * ((↑t - ↑a) / (↑b - ↑a)))

theorem circleParam_integrand_const (z₀ : ℂ) (r : ℝ) (hr : 0 < r) (a b : ℝ) (hab : a < b) (t : ℝ) : (circleParam z₀ r a b t - z₀)⁻¹ * deriv (circleParam z₀ r a b) t = 2 * ↑Real.pi * Complex.I / (↑b - ↑a)

theorem circleParam_winding_eq_one (z₀ : ℂ) (r : ℝ) (hr : 0 < r) (a b : ℝ) (hab : a < b) : generalizedWindingNumber' (circleParam z₀ r a b) a b z₀ = 1

The winding number of a CCW circle around its center is 1.

noncomputable def circleParamCW (z₀ : ℂ) (r a b t : ℝ) : ℂ

Clockwise circle parameterization: reversal of circleParam. circleParamCW z₀ r a b t = circleParam z₀ r a b (a + b - t)

Equations

• circleParamCW z₀ r a b t = circleParam z₀ r a b (a + b - t)

theorem circleParamCW_continuous (z₀ : ℂ) (r a b : ℝ) : Continuous (circleParamCW z₀ r a b)

theorem circleParamCW_closed (z₀ : ℂ) (r a b : ℝ) (hab : a < b) : circleParamCW z₀ r a b a = circleParamCW z₀ r a b b

theorem circleParamCW_dist (z₀ : ℂ) (r : ℝ) (hr : 0 ≤ r) (a b : ℝ) (hab : a < b) (t : ℝ) : ‖circleParamCW z₀ r a b t - z₀‖ = r

theorem circleParam_differentiable (z₀ : ℂ) (r a b : ℝ) : Differentiable ℝ (circleParam z₀ r a b)

theorem circleParamCW_differentiable (z₀ : ℂ) (r a b : ℝ) : Differentiable ℝ (circleParamCW z₀ r a b)

theorem circleParamCW_hasDerivAt (z₀ : ℂ) (r a b : ℝ) (hab : a < b) (t : ℝ) : HasDerivAt (circleParamCW z₀ r a b) (-(↑r * (2 * ↑Real.pi * Complex.I / (↑b - ↑a)) * Complex.exp (2 * ↑Real.pi * Complex.I * ((↑(a + b - t) - ↑a) / (↑b - ↑a))))) t

theorem circleParamCW_deriv (z₀ : ℂ) (r a b : ℝ) (hab : a < b) (t : ℝ) : deriv (circleParamCW z₀ r a b) t = -(↑r * (2 * ↑Real.pi * Complex.I / (↑b - ↑a)) * Complex.exp (2 * ↑Real.pi * Complex.I * ((↑(a + b - t) - ↑a) / (↑b - ↑a))))

theorem circleParamCW_integrand_neg (z₀ : ℂ) (r : ℝ) (hr : 0 < r) (a b : ℝ) (hab : a < b) (t : ℝ) : (circleParamCW z₀ r a b t - z₀)⁻¹ * deriv (circleParamCW z₀ r a b) t = -(2 * ↑Real.pi * Complex.I / (↑b - ↑a))

theorem circleParamCW_winding_eq_neg_one (z₀ : ℂ) (r : ℝ) (hr : 0 < r) (a b : ℝ) (hab : a < b) : generalizedWindingNumber' (circleParamCW z₀ r a b) a b z₀ = -1

Winding number of a CW circle around its center is -1.

theorem winding_of_S1_curve_eq_degree (z₀ : ℂ) (a b : ℝ) (_hab : a < b) (n : ℤ) (θ : ℝ → ℝ) (hθ_diff : Differentiable ℝ θ) (hθ_deriv_cont : Continuous (deriv θ)) (hθ_change : θ b - θ a = 2 * Real.pi * ↑n) : have γ := fun (t : ℝ) => z₀ + Complex.exp (Complex.I * ↑(θ t)); generalizedWindingNumber' γ a b z₀ = ↑n

For a C¹ curve on S¹ with angle lift θ, the winding number equals the degree.