OAI/Analysis/IrrationalRotation/Rotation/CircleParameterConsequences.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleParameterLaws.shifted_K_pos line 16
2. theorem OAI.Invariant233.CircleParameterLaws.shifted_K_double line 19
3. theorem OAI.Invariant233.CircleParameterLaws.summable_reciprocal line 23
4. theorem OAI.Invariant233.CircleParameterLaws.reciprocal_tail_bound line 26
5. theorem OAI.Invariant233.CircleParameterLaws.summable_partition_cost line 31
6. theorem OAI.Invariant233.CircleParameterLaws.tendsto_sampling_horizon line 42