OAI/NumberTheory/Ostmann/QuadraticSieveGcdSeparationBlocks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.divisorPairJacobiRow line 8
2. theorem OAI.Ostmann.QuadraticSieve.divisorPairJacobiRow_norm_sq_le line 12
3. theorem OAI.Ostmann.QuadraticSieve.sum_divisorPairWeightedEnergy_le line 38
4. theorem OAI.Ostmann.QuadraticSieve.sum_divisorPairWeightedEnergy_snd_le line 46
5. theorem OAI.Ostmann.QuadraticSieve.quotientNormMax_le_oddSquarefreeUpTo line 54
6. theorem OAI.Ostmann.QuadraticSieve.divisorPairJacobiRow_norm_sq_le_rpow line 70