OAI/NumberTheory/Ostmann/SharpSieve.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sum_trigPoly_sq_le line 17
2. theorem OAI.Ostmann.sum_trigPoly_sq_le_32 line 46
3. theorem OAI.Ostmann.sum_circleTrigPoly_sq_le line 60
4. theorem OAI.Ostmann.sum_trigPoly_sq_reducedFrequency_le line 70
5. theorem OAI.Ostmann.trigPoly_normalizedCoefficients line 84
6. theorem OAI.Ostmann.sum_normalizedExpSum_sq_reducedFrequency_le line 104
7. theorem OAI.Ostmann.sum_normalizedExpSum_sq_le_of_le_sq line 113