Arc Calculus

General-purpose API for unit circle arc parameterizations and their properties. Used for computing winding numbers, distances, and derivatives along circular arcs.

Main definitions

• unitArc - parameterization of a unit circle arc from angle θ₁ to θ₂

Main results

• unitArc_norm - points on the arc have norm 1
• unitArc_hasDerivAt - derivative formula for the arc
• exp_sub_norm_sq - distance formula between arc points via cosine
• sin_pos_of_mem_Ioo_zero_pi - sin is positive on (0, π)

noncomputable def ArcCalculus.unitArc (θ₁ θ₂ a b t : ℝ) : ℂ

Unit circle arc from angle θ₁ to θ₂, linearly parameterized on [a,b].

Equations

• ArcCalculus.unitArc θ₁ θ₂ a b t = Complex.exp (↑(θ₁ + (t - a) / (b - a) * (θ₂ - θ₁)) * Complex.I)

theorem ArcCalculus.unitArc_norm (θ₁ θ₂ a b t : ℝ) : ‖unitArc θ₁ θ₂ a b t‖ = 1

Points on the unit arc have norm 1.

theorem ArcCalculus.unitArc_at_start (θ₁ θ₂ a b : ℝ) : unitArc θ₁ θ₂ a b a = Complex.exp (↑θ₁ * Complex.I)

The arc starts at exp(iθ₁).

theorem ArcCalculus.unitArc_at_end (θ₁ θ₂ a b : ℝ) (hab : a ≠ b) : unitArc θ₁ θ₂ a b b = Complex.exp (↑θ₂ * Complex.I)

The arc ends at exp(iθ₂).

theorem ArcCalculus.unitArc_continuous (θ₁ θ₂ a b : ℝ) : Continuous (unitArc θ₁ θ₂ a b)

The unit arc is continuous.

theorem ArcCalculus.unitArc_hasDerivAt (θ₁ θ₂ a b t : ℝ) (hab : a < b) : HasDerivAt (unitArc θ₁ θ₂ a b) (unitArc θ₁ θ₂ a b t * (↑((θ₂ - θ₁) / (b - a)) * Complex.I)) t

Derivative of the unit arc.

theorem ArcCalculus.exp_sub_norm_sq (θ₁ θ₂ : ℝ) : ‖Complex.exp (↑θ₁ * Complex.I) - Complex.exp (↑θ₂ * Complex.I)‖ ^ 2 = 2 - 2 * Real.cos (θ₁ - θ₂)

Key distance formula: squared norm of difference of two points on the unit circle.

theorem ArcCalculus.sin_pos_of_mem_Ioo_zero_pi {θ : ℝ} (hθ : θ ∈ Set.Ioo 0 Real.pi) : 0 < Real.sin θ

sin is positive on the open interval (0, π).

theorem ArcCalculus.abs_cos_le_half_of_mem_Icc {θ : ℝ} (hθ : θ ∈ Set.Icc (Real.pi / 3) (2 * Real.pi / 3)) : |Real.cos θ| ≤ 1 / 2

|cos θ| ≤ 1/2 for θ ∈ [π/3, 2π/3].