OAI/Analysis/IrrationalRotation/Model/CircleWeights.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.CircleWeights.representative line 11
2. def OAI.Invariant233.CircleWeights.coordinate line 14
3. def OAI.Invariant233.CircleWeights.phase line 17
4. def OAI.Invariant233.CircleWeights.rotate line 20
5. def OAI.Invariant233.CircleWeights.floorCost line 23
6. def OAI.Invariant233.CircleWeights.cocycle line 27
7. def OAI.Invariant233.CircleWeights.weight line 31