OAI/Analysis/IrrationalRotation/Rotation/CircleFiberDecay.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantProjection.CircleFiberDecay.Circle line 14
2. lemma OAI.InvariantProjection.CircleFiberDecay.coordinate_product_eq line 16
3. theorem OAI.InvariantProjection.CircleFiberDecay.norm_fiber_power_le line 25
4. theorem OAI.InvariantProjection.CircleFiberDecay.all_rates_fiber_decay line 38
5. theorem OAI.InvariantProjection.CircleFiberDecay.fiber_norm_quasinilpotent line 50