OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/SieveTriangleKernelErrorAt.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.OrdinarySelbergWeights.sieveTriangleKernel_error_at_scale line 16
2. lemma OAI.OrdinarySelbergWeights.sieveTriangleKernel_norm_at_scale line 59
3. theorem OAI.OrdinarySelbergWeights.sparse_rough_gram_row_at_scale line 74
4. theorem OAI.OrdinarySelbergWeights.rough_mellin_energy_at_scale line 108
5. theorem OAI.OrdinarySelbergWeights.rough_card_bound_at_scale line 142
6. theorem OAI.OrdinarySelbergWeights.rough_harmonic_energy_at_scale line 176
7. theorem OAI.OrdinarySelbergWeights.signed_product_energy_at_scale line 210