OAI/NumberTheory/Ostmann/QuadraticSieveCoprimePoissonErrors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.largeDivisorError line 10
2. def OAI.Ostmann.QuadraticSieve.smallDivisorError line 14
3. def OAI.Ostmann.QuadraticSieve.middleDivisorError line 18
4. theorem OAI.Ostmann.QuadraticSieve.norm_sum_moebius_mul_le line 22
5. theorem OAI.Ostmann.QuadraticSieve.mul_div_pow_succ line 31
6. theorem OAI.Ostmann.QuadraticSieve.ratio_pow_le_inv_pow line 36
7. theorem OAI.Ostmann.QuadraticSieve.large_cutoff_ratio_bound line 50
8. theorem OAI.Ostmann.QuadraticSieve.largeDivisorError_bound line 67
9. theorem OAI.Ostmann.QuadraticSieve.cutoff_power_identity line 97
10. theorem OAI.Ostmann.QuadraticSieve.smallDivisorError_bound line 102
11. theorem OAI.Ostmann.QuadraticSieve.middleDivisorError_bound line 141