OAI/NumberTheory/DirichletL/CubicSieve/Elements.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CubicSieve.elementCharacter line 11
2. theorem OAI.SevenEighths.CubicSieve.elementCharacter_norm_le_one line 16
3. theorem OAI.SevenEighths.CubicSieve.element_block_energy_le line 23
4. def OAI.SevenEighths.CubicSieve.goodPart line 52
5. def OAI.SevenEighths.CubicSieve.badPart line 54
6. theorem OAI.SevenEighths.CubicSieve.goodPart_admissible line 57
7. theorem OAI.SevenEighths.CubicSieve.badPart_mul_goodPart line 61
8. def OAI.SevenEighths.CubicSieve.extractedGenerator line 64
9. theorem OAI.SevenEighths.CubicSieve.span_extractedGenerator line 70
10. theorem OAI.SevenEighths.CubicSieve.element_cubic_extraction line 93
11. theorem OAI.SevenEighths.CubicSieve.badPart_sector line 101