OAI/NumberTheory/Ostmann/QuadraticSieveWeightedSmoothingDyadic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.dyadicSquarefreeRows line 7
2. theorem OAI.Ostmann.QuadraticSieve.mem_dyadicSquarefreeRows line 10
3. theorem OAI.Ostmann.QuadraticSieve.squarefreeKernel_of_squarefree line 19
4. theorem OAI.Ostmann.QuadraticSieve.dyadicRow_mem_smoothingRows line 22
5. theorem OAI.Ostmann.QuadraticSieve.smoothingWeight_one_dyadic line 32
6. theorem OAI.Ostmann.QuadraticSieve.numeratorEnergy_dyadic_le_smoothingEnergy line 45
7. theorem OAI.Ostmann.QuadraticSieve.numeratorEnergy_dyadic_le_smoothingNorm line 66