OAI/Analysis/IrrationalRotation/Rotation/CircleOrderedSharpness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.CircleOrderedRigidity.rationalPeriodGraph line 11
2. theorem OAI.Invariant233.CircleOrderedRigidity.measurable_rationalPeriodPair line 15
3. theorem OAI.Invariant233.CircleOrderedRigidity.rationalPeriodGraph_fst line 20
4. theorem OAI.Invariant233.CircleOrderedRigidity.rationalPeriodGraph_snd line 26
5. theorem OAI.Invariant233.CircleOrderedRigidity.rationalPeriodGraph_probability line 33
6. theorem OAI.Invariant233.CircleOrderedRigidity.first_frequency_gt_one line 38
7. theorem OAI.Invariant233.CircleOrderedRigidity.rationalPeriod_ne_zero line 42
8. theorem OAI.Invariant233.CircleOrderedRigidity.rationalPeriodGraph_ae_coordinate_eq line 55
9. theorem OAI.Invariant233.CircleOrderedRigidity.rationalPeriodGraph_ae_ne line 74
10. theorem OAI.Invariant233.CircleOrderedRigidity.exists_ordered_haar_law_off_diagonal line 85