OAI/NumberTheory/DirichletL/Hecke/PrimeAnnular.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckePrimeAnnular.annulusSet line 13
2. def OAI.SevenEighths.HeckePrimeAnnular.annularWeight line 15
3. def OAI.SevenEighths.HeckePrimeAnnular.primePolynomial line 18
4. theorem OAI.SevenEighths.HeckePrimeAnnular.annular_support line 22
5. theorem OAI.SevenEighths.HeckePrimeAnnular.log_polynomial_eq_finite line 35
6. theorem OAI.SevenEighths.HeckePrimeAnnular.fixed_profile_norm_bound line 70
7. theorem OAI.SevenEighths.HeckePrimeAnnular.extraction_bound line 85