OAI/NumberTheory/DirichletL/Descent/HybridReduction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.finite_inverse_cubic_energy line 12
2. theorem OAI.SevenEighths.InverseMoment.hybrid_quadratic_reduction line 45
3. theorem OAI.SevenEighths.InverseMoment.cubic_product_row_bound_of_sieve line 83
4. theorem OAI.SevenEighths.InverseMoment.cubic_product_row_sieve_norm line 120
5. theorem OAI.SevenEighths.InverseMoment.hybrid_fixed_block_sieve_norm line 137