OAI/NumberTheory/Ostmann/QuadraticSieveComplementAggregateKernels.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.complementLargeScalar line 12
2. def OAI.Ostmann.QuadraticSieve.complementFourierScalar line 15
3. def OAI.Ostmann.QuadraticSieve.complementFourierBound line 22
4. theorem OAI.Ostmann.QuadraticSieve.complementFourierBound_pos line 25
5. theorem OAI.Ostmann.QuadraticSieve.complementLargeScalar_norm_le line 30
6. theorem OAI.Ostmann.QuadraticSieve.complementFourierScalar_norm_le line 35
7. theorem OAI.Ostmann.QuadraticSieve.complementaryLargeCorrection_eq_scalar line 51
8. theorem OAI.Ostmann.QuadraticSieve.complementaryFourierCorrection_eq_scalar line 93