Download PDFOpen PDF in browser

Formalizing Rotation Number and Its Properties in Lean

EasyChair Preprint 6168

5 pagesDate: July 27, 2021

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

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