OAI/Analysis/IrrationalRotation/Rotation/CircleWeightDecay.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantProjection.CircleWeightDecay.Circle line 17
2. theorem OAI.InvariantProjection.CircleWeightDecay.all_rates_decay line 19
3. def OAI.InvariantProjection.CircleWeightDecay.orbitProductC line 39
4. lemma OAI.InvariantProjection.CircleWeightDecay.orbitProductC_apply line 43
5. lemma OAI.InvariantProjection.CircleWeightDecay.orbitProductC_nonneg line 47
6. theorem OAI.InvariantProjection.CircleWeightDecay.all_rates_norm_decay line 53
7. theorem OAI.InvariantProjection.CircleWeightDecay.tendsto_norm_root_zero line 67
8. lemma OAI.InvariantProjection.CircleWeightDecay.circleMeasure_eq_haar line 76
9. theorem OAI.InvariantProjection.CircleWeightDecay.all_rates_decay_of_isContinuousCircleWeight line 82