OAI/NumberTheory/Ostmann/QuadraticSieveSmoothingGcdLattice.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.QuadraticSieve.sieveWeight_zero_outside_rows line 9
2. lemma OAI.Ostmann.QuadraticSieve.tsum_positive_nat_eq_integer line 24
3. def OAI.Ostmann.QuadraticSieve.smoothingCoprimeLatticeTerm line 37
4. lemma OAI.Ostmann.QuadraticSieve.smoothingCoprimeLatticeTerm_zero_outside line 41
5. lemma OAI.Ostmann.QuadraticSieve.smoothingCoprimeLatticeTerm_summable line 47
6. lemma OAI.Ostmann.QuadraticSieve.odd_square_jacobi_eq_coprime line 52
7. theorem OAI.Ostmann.QuadraticSieve.complementarySchwartzSum_eq_small_lattice line 61
8. theorem OAI.Ostmann.QuadraticSieve.smoothing_lattice_sub_complement line 86