OAI/NumberTheory/Ostmann/QuadraticSieveComplementCorrelations.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.complementLargeKernel line 9
2. def OAI.Ostmann.QuadraticSieve.complementFourierKernel line 12
3. def OAI.Ostmann.QuadraticSieve.complementaryLargeCorrection line 18
4. def OAI.Ostmann.QuadraticSieve.complementaryFourierCorrection line 25
5. theorem OAI.Ostmann.QuadraticSieve.complementaryPoissonMain_components line 32
6. theorem OAI.Ostmann.QuadraticSieve.complementaryCorrelationMain_eq line 72
7. theorem OAI.Ostmann.QuadraticSieve.complementaryCorrelationMain_eq_of_oddSquarefree line 120