OAI/NumberTheory/DirichletL/Moments/Extraction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentExtraction.idealRectangle_extract line 12
2. theorem OAI.SevenEighths.CenteredMomentExtraction.extracted_rectangle_coefficient line 21
3. theorem OAI.SevenEighths.CenteredMomentExtraction.extracted_rectangle_sum line 35
4. theorem OAI.SevenEighths.CenteredMomentExtraction.extracted_product_scale line 48
5. theorem OAI.SevenEighths.CenteredMomentExtraction.idealWeight_norm_le_one line 56
6. theorem OAI.SevenEighths.CenteredMomentExtraction.normalized_extracted_rectangle_estimate line 67
7. theorem OAI.SevenEighths.CenteredMomentExtraction.centered_slot_allocation line 113
8. theorem OAI.SevenEighths.CenteredMomentExtraction.prime_slot_allocation line 135