OAI/Analysis/IrrationalRotation/Rotation/UniformRotationAverage.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InvariantProjection.UniformRotationAverage.Circle line 19
2. abbrev OAI.InvariantProjection.UniformRotationAverage.CSpace line 20
3. def OAI.InvariantProjection.UniformRotationAverage.translate line 22
4. def OAI.InvariantProjection.UniformRotationAverage.translateL line 25
5. def OAI.InvariantProjection.UniformRotationAverage.averageL line 28
6. lemma OAI.InvariantProjection.UniformRotationAverage.averageL_apply line 31
7. lemma OAI.InvariantProjection.UniformRotationAverage.norm_averageL_apply_le line 35
8. lemma OAI.InvariantProjection.UniformRotationAverage.averageL_lipschitz line 55
9. def OAI.InvariantProjection.UniformRotationAverage.meanL line 61
10. lemma OAI.InvariantProjection.UniformRotationAverage.meanL_apply line 66
11. def OAI.InvariantProjection.UniformRotationAverage.convergentSubmodule line 75
12. lemma OAI.InvariantProjection.UniformRotationAverage.isClosed_convergentSubmodule line 87
13. lemma OAI.InvariantProjection.UniformRotationAverage.fourier_translate line 92
14. lemma OAI.InvariantProjection.UniformRotationAverage.averageL_fourier line 97
15. lemma OAI.InvariantProjection.UniformRotationAverage.norm_geometric_sum_le line 106
16. lemma OAI.InvariantProjection.UniformRotationAverage.tendsto_averageL_fourier_zero line 114
17. lemma OAI.InvariantProjection.UniformRotationAverage.fourier_ne_one_of_irrational line 127
18. lemma OAI.InvariantProjection.UniformRotationAverage.meanL_fourier_of_ne_zero line 140
19. lemma OAI.InvariantProjection.UniformRotationAverage.fourier_mem_convergentSubmodule line 149
20. theorem OAI.InvariantProjection.UniformRotationAverage.tendsto_averageL line 168
21. theorem OAI.InvariantProjection.UniformRotationAverage.tendstoUniformly_complex line 181
22. theorem OAI.InvariantProjection.UniformRotationAverage.tendstoUniformly_real line 192