OAI/NumberTheory/Ostmann/ZeroDensity/FiniteDetector.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.ZeroDensity.twistedPolynomial line 13
2. theorem OAI.Ostmann.ZeroDensity.LSeries_eq_twistedPolynomial_of_support line 17
3. theorem OAI.Ostmann.ZeroDensity.LSeries_truncate_eq_twistedPolynomial line 36
4. def OAI.Ostmann.ZeroDensity.detectorPolynomial line 46
5. theorem OAI.Ostmann.ZeroDensity.mollifier_polynomial_split line 49
6. theorem OAI.Ostmann.ZeroDensity.finite_mollifier_identity line 86
7. theorem OAI.Ostmann.ZeroDensity.norm_moebius_le_one line 97
8. theorem OAI.Ostmann.ZeroDensity.norm_mollifierPolynomial_le line 100
9. theorem OAI.Ostmann.ZeroDensity.detector_large_of_small_product line 124