Absolute continuity of circleMap

The complex circle parametrization circleMap c R is Lipschitz (lipschitzWith_circleMap), hence absolutely continuous on every parameter interval.

theorem TauCeti.absolutelyContinuousOnInterval_circleMap (c : ℂ) (R a b : ℝ) : AbsolutelyContinuousOnInterval (circleMap c R) a b

The circle parametrization circleMap c R is absolutely continuous on every real parameter interval, for arbitrary center c and signed radius R.