Formalizing Rotation Number and Its Properties in Lean

EasyChair Preprint no. 6168

Abstract

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

@Booklet{EasyChair:6168,
  author = {Yury Kudryashov},
  title = {Formalizing Rotation Number and Its Properties in Lean},
  howpublished = {EasyChair Preprint no. 6168},

  year = {EasyChair, 2021}}