Formalizing Rotation Number and Its Properties in Lean

EasyChair Preprint 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: Rotation number, circle homeomorphisms, dynamical systems

@booklet{EasyChair:6168,
  author    = {Yury Kudryashov},
  title     = {Formalizing Rotation Number and Its Properties in Lean},
  howpublished = {EasyChair Preprint 6168},
  year      = {EasyChair, 2021}}