OAI/Analysis/IrrationalRotation/Rotation/RotationMoments.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.Rotation.unitaryU line 14
2. def OAI.Invariant233.Rotation.unitaryV line 16
3. def OAI.Invariant233.Rotation.shiftUnitaryHom line 19
4. theorem OAI.Invariant233.Rotation.unitaryU_zpow line 25
5. theorem OAI.Invariant233.Rotation.fourier_zero_map line 35
6. theorem OAI.Invariant233.Rotation.fourier_add_map line 39
7. def OAI.Invariant233.Rotation.characterUnitaryHom line 44
8. theorem OAI.Invariant233.Rotation.unitaryV_zpow line 58
9. theorem OAI.Invariant233.Rotation.vacuumFunctional_shift_representation line 68
10. theorem OAI.Invariant233.Rotation.shift_representation_vacuum_ae line 91
11. theorem OAI.Invariant233.Rotation.unitary_zpow_mem_algebra line 112
12. theorem OAI.Invariant233.Rotation.unitary_monomial_mem_algebra line 124
13. theorem OAI.Invariant233.Rotation.integral_fourier_circle line 131
14. theorem OAI.Invariant233.Rotation.vacuumFunctional_unitary_zpowers line 141
15. def OAI.Invariant233.Rotation.monomialVector line 150
16. theorem OAI.Invariant233.Rotation.monomialVector_ae line 154
17. theorem OAI.Invariant233.Rotation.inner_monomialVector line 162
18. theorem OAI.Invariant233.Rotation.orthonormal_monomialVector line 188