OAI/Probability/BinarySweep/Representations/IsotypicProjectionMoment.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.euclidean_pow line 17
2. lemma OAI.BinaryCoordinateSweeps.projected_gram_power line 23
3. lemma OAI.BinaryCoordinateSweeps.trace_mul_projection line 38
4. def OAI.BinaryCoordinateSweeps.Signed.signedAverage line 55
5. lemma OAI.BinaryCoordinateSweeps.Signed.signedAverage_linear line 58
6. lemma OAI.BinaryCoordinateSweeps.Signed.isotypicProjection_commutes_average line 63
7. theorem OAI.BinaryCoordinateSweeps.Signed.local_projected_moment line 69
8. lemma OAI.BinaryCoordinateSweeps.Signed.hilbert_multiplicity_bound line 89
9. theorem OAI.BinaryCoordinateSweeps.Signed.local_projected_moment_le line 100
10. abbrev OAI.BinaryCoordinateSweeps.Fourier.RegularSpace line 122
11. def OAI.BinaryCoordinateSweeps.Fourier.regularMap line 124
12. def OAI.BinaryCoordinateSweeps.Fourier.regular line 129
13. lemma OAI.BinaryCoordinateSweeps.Fourier.regular_apply line 135
14. lemma OAI.BinaryCoordinateSweeps.Fourier.regular_unitary line 138
15. lemma OAI.BinaryCoordinateSweeps.Fourier.regular_character line 143
16. lemma OAI.BinaryCoordinateSweeps.Fourier.regular_multiplicity line 159
17. lemma OAI.BinaryCoordinateSweeps.Fourier.regular_average_apply line 172
18. lemma OAI.BinaryCoordinateSweeps.Fourier.regular_moment_one line 176