OAI/Analysis/IrrationalRotation/Sampling/CircleRationalSamplingIndex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.exists_nat_rational_representative line 8
2. theorem OAI.Invariant233.CircleParameterLaws.rational_shift_later_denominator line 33
3. theorem OAI.Invariant233.CircleParameterLaws.exists_rational_sampling_index line 52
4. theorem OAI.Invariant233.CircleParameterLaws.exists_rational_sampling_index_of_late line 58