OAI/NumberTheory/DirichletL/CubicSieve/ExtractionBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CubicSieve.extracted_parts_ne_zero line 11
2. theorem OAI.SevenEighths.CubicSieve.goodPart_norm_le line 19
3. theorem OAI.SevenEighths.CubicSieve.full_element_extraction_norm_bound line 23
4. theorem OAI.SevenEighths.CubicSieve.cubePart_norm_le_of_block line 88
5. theorem OAI.SevenEighths.CubicSieve.full_element_dyadic_block_bound line 108