OAI/NumberTheory/Ostmann/QuadraticSieveGcdSeparationProduct.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.coprimeProductDivisorJacobiRow line 8
2. theorem OAI.Ostmann.QuadraticSieve.coprimeProductDivisorJacobiRow_eq line 13
3. def OAI.Ostmann.QuadraticSieve.divisorNormEnergy line 19
4. lemma OAI.Ostmann.QuadraticSieve.divisorNormEnergy_nonneg line 23
5. theorem OAI.Ostmann.QuadraticSieve.coprimeProductDivisorJacobiRow_norm_sq_le line 29
6. def OAI.Ostmann.QuadraticSieve.quotientNormMax line 65
7. lemma OAI.Ostmann.QuadraticSieve.quotientNormMax_nonneg line 69
8. lemma OAI.Ostmann.QuadraticSieve.quadraticNorm_le_quotientNormMax line 72
9. lemma OAI.Ostmann.QuadraticSieve.divisorNormEnergy_le line 77
10. theorem OAI.Ostmann.QuadraticSieve.coprimeProductDivisorJacobiRow_norm_sq_le_rpow line 88