OAI/NumberTheory/Ostmann/QuadraticSieveNorm.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticSieve.jacobi_row_energy_le line 7
2. theorem OAI.Ostmann.QuadraticSieve.jacobiEnergy_le_card_mul line 19
3. def OAI.Ostmann.QuadraticSieve.quadraticNorm line 26
4. theorem OAI.Ostmann.QuadraticSieve.quadratic_ratios_bddAbove line 29
5. theorem OAI.Ostmann.QuadraticSieve.quadraticNorm_nonneg line 39
6. theorem OAI.Ostmann.QuadraticSieve.jacobiEnergy_le_quadraticNorm line 44
7. theorem OAI.Ostmann.QuadraticSieve.quadraticNorm_le_of_bound line 52
8. theorem OAI.Ostmann.QuadraticSieve.quadraticNorm_le_card_mul line 63
9. theorem OAI.Ostmann.QuadraticSieve.jacobiEnergy_mono_rows line 67
10. theorem OAI.Ostmann.QuadraticSieve.quadraticNorm_mono_rows line 71