OAI/NumberTheory/DirichletL/CubicSieve/ExtractionOptimization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CubicSieve.cube_scale_power line 8
2. lemma OAI.SevenEighths.CubicSieve.extracted_monomial_le line 18
3. lemma OAI.SevenEighths.CubicSieve.extracted_linear_le line 30
4. lemma OAI.SevenEighths.CubicSieve.extraction_selected_shape line 37
5. theorem OAI.SevenEighths.CubicSieve.extraction_min_shape line 68
6. lemma OAI.SevenEighths.CubicSieve.cubic_cross_shape_absorb line 90
7. theorem OAI.SevenEighths.CubicSieve.extraction_min_two_power line 124