OAI/NumberTheory/Ostmann/Conclusion/PermutationSymmetrization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Conclusion.permuteTuple line 9
2. def OAI.Ostmann.Conclusion.tuplePermutation line 12
3. def OAI.Ostmann.Conclusion.jointWeight line 18
4. theorem OAI.Ostmann.Conclusion.jointWeight_permute line 21
5. def OAI.Ostmann.Conclusion.finiteCorrelation line 26
6. def OAI.Ostmann.Conclusion.symmetrizedAmplitude line 30
7. theorem OAI.Ostmann.Conclusion.finiteCorrelation_permute line 34
8. theorem OAI.Ostmann.Conclusion.finiteCorrelation_sum line 42
9. theorem OAI.Ostmann.Conclusion.finiteCorrelation_symmetrize line 56
10. theorem OAI.Ostmann.Conclusion.norm_sum_sq_eq_pair_sum line 79
11. theorem OAI.Ostmann.Conclusion.weighted_cauchy_schwarz line 89
12. theorem OAI.Ostmann.Conclusion.finiteCorrelation_cauchy_schwarz line 119