OAI/Analysis/IrrationalRotation/PrescribedAngle.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Continuous counterexamples for every prescribed irrational angle.

  1. theorem OAI.Invariant233.publishedRotationSpectralInput_of_irrational line 9
  2. theorem OAI.Invariant233.Results.prescribed_irrational_counterexample line 17

    Distinct definitions of this name: ComparatorChallenges/IrrationalRotation.lean:838 (different declaration text). Qualify references as OAI.Invariant233.Results.prescribed_irrational_counterexample@path.

  3. theorem OAI.Invariant233.Results.prescribed_irrational_weight line 23