OAI/NumberTheory/Ostmann/QuadraticCenter/LocalCorrelationCentered.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.norm_unitaryDFT_le_sqrt line 10
2. theorem OAI.Ostmann.QuadraticCenter.norm_centeredIndicator_le_one line 30
3. def OAI.Ostmann.QuadraticCenter.centeredProduct line 38
4. theorem OAI.Ostmann.QuadraticCenter.norm_centeredProduct_le_one line 44
5. def OAI.Ostmann.QuadraticCenter.centeredProductTransform line 56
6. theorem OAI.Ostmann.QuadraticCenter.norm_centeredProductTransform_le_sqrt line 62