OAI/NumberTheory/Ostmann/QuadraticSieveLargeGcdBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.largeGcdCoefficients line 8
2. theorem OAI.Ostmann.QuadraticSieve.coefficientEnergy_largeGcdCoefficients_le line 11
3. theorem OAI.Ostmann.QuadraticSieve.sum_coefficientEnergy_largeGcdCoefficients_le line 23
4. theorem OAI.Ostmann.QuadraticSieve.gcdJacobiRow_norm_le_divisor_energies line 32
5. def OAI.Ostmann.QuadraticSieve.weightedGcdMass line 52
6. lemma OAI.Ostmann.QuadraticSieve.weightedGcdMass_nonneg line 56
7. theorem OAI.Ostmann.QuadraticSieve.weightedGcdMass_le_quotient_norm line 61
8. theorem OAI.Ostmann.QuadraticSieve.weighted_quotient_norm_le_prefix line 85
9. theorem OAI.Ostmann.QuadraticSieve.sum_weightedGcdMass_le_rpow line 96