Download PDFOpen PDF in browser

Formalizing Rotation Number and Its Properties in Lean

EasyChair Preprint no. 6168

5 pagesDate: July 27, 2021


Rotation number is the key numerical invariant of an orientation preserving circle homeomorphism. This paper describes the current state of an ongoing project with aim to formalize various facts about circle dynamics in Lean. Currently, the formalized material includes the definition and basic properties of the translation number of a lift of a circle homeomorphism to the real line. I also formalized a theorem by É.~Ghys that gives a necessary and sufficient condition for two actions of a group on the circle by homeomorphism to be semiconjugate to each other.

Keyphrases: circle homeomorphisms, dynamical systems, Rotation number

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Yury Kudryashov},
  title = {Formalizing Rotation Number and Its Properties in Lean},
  howpublished = {EasyChair Preprint no. 6168},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser