OAI/NumberTheory/Ostmann/QuadraticSieveWeightedNorm.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticSieve.weightedNumeratorEnergy line 7
2. theorem OAI.Ostmann.QuadraticSieve.numerator_row_energy_le line 11
3. theorem OAI.Ostmann.QuadraticSieve.weightedNumeratorEnergy_le_card_mul line 23
4. lemma OAI.Ostmann.QuadraticSieve.weightedNumeratorEnergy_nonneg line 35
5. def OAI.Ostmann.QuadraticSieve.weightedNumeratorNorm line 40
6. lemma OAI.Ostmann.QuadraticSieve.weighted_numerator_ratios_bddAbove line 43
7. theorem OAI.Ostmann.QuadraticSieve.weightedNumeratorNorm_nonneg line 54
8. theorem OAI.Ostmann.QuadraticSieve.weightedNumeratorEnergy_le_norm line 60
9. theorem OAI.Ostmann.QuadraticSieve.weightedNumeratorNorm_le_of_bound line 69
10. theorem OAI.Ostmann.QuadraticSieve.weightedNumeratorEnergy_supportCoefficients line 81
11. theorem OAI.Ostmann.QuadraticSieve.weightedNumeratorNorm_mono_columns line 98