OAI/Analysis/IrrationalRotation/Rotation/RotationDecay.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantProjection.RotationDecay.truncatedLog line 19
2. def OAI.InvariantProjection.RotationDecay.orbitProduct line 22
3. lemma OAI.InvariantProjection.RotationDecay.le_exp_truncatedLog line 25
4. lemma OAI.InvariantProjection.RotationDecay.orbitProduct_nonneg line 30
5. lemma OAI.InvariantProjection.RotationDecay.orbitProduct_le_exp_sum_truncatedLog line 35
6. lemma OAI.InvariantProjection.RotationDecay.orbitProduct_le_exp_of_sum_le line 43
7. lemma OAI.InvariantProjection.RotationDecay.orbitProduct_le_exp_of_average_le line 49
8. lemma OAI.InvariantProjection.RotationDecay.eventually_orbitProduct_le_exp line 59
9. theorem OAI.InvariantProjection.RotationDecay.all_rates_orbitProduct_decay line 74