circleMap #
This file defines the circle map
Main definitions #
circleMap c R
: the exponential map .
Tags #
@[deprecated norm_circleMap_zero (since := "2025-02-17")]
Alias of norm_circleMap_zero
.
@[deprecated circleMap_notMem_ball (since := "2025-05-23")]
Alias of circleMap_notMem_ball
.
circleMap
is 2π
-periodic.