OAI/NumberTheory/DirichletL/CubicSieve/CompactDescent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CubicSieve.majorant_radial_summable line 13
2. lemma OAI.SevenEighths.CubicSieve.majorant_rescale line 19
3. lemma OAI.SevenEighths.CubicSieve.dividedMajorant_tsum line 27
4. lemma OAI.SevenEighths.CubicSieve.majorant_coprime_tsum line 49
5. lemma OAI.SevenEighths.CubicSieve.compact_gcd_mobius_descent line 75
6. lemma OAI.SevenEighths.CubicSieve.gcdPool_cubic_admissible line 101
7. lemma OAI.SevenEighths.CubicSieve.gcdPool_subset_columnDivisorPool line 107
8. theorem OAI.SevenEighths.CubicSieve.finite_energy_le_compact_descendants line 114