OAI/NumberTheory/Ostmann/QuadraticSieveSmoothingColumnDyadicBasic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticSieve.smoothing_column_cauchy line 10
2. theorem OAI.Ostmann.QuadraticSieve.smoothingWeight_sum_le line 16
3. theorem OAI.Ostmann.QuadraticSieve.smoothingNorm_le_trivial line 31
4. theorem OAI.Ostmann.QuadraticSieve.binarySquarefreeRows_zero line 40
5. theorem OAI.Ostmann.QuadraticSieve.smoothingNorm_binary_zero_le line 51
6. theorem OAI.Ostmann.QuadraticSieve.binarySquarefreeRows_positive_data line 56