OAI/NumberTheory/DirichletL/Descent/SieveComposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.bounded_finset_coefficient_sum_sq line 11
2. theorem OAI.SevenEighths.InverseMoment.bounded_coefficient_sum_sq line 20
3. theorem OAI.SevenEighths.InverseMoment.positive_triple_enlarge line 26
4. theorem OAI.SevenEighths.InverseMoment.column_fiber_sieve line 53
5. theorem OAI.SevenEighths.InverseMoment.quadratic_cubic_composition line 92