OAI/NumberTheory/DirichletL/Hecke/DetectorCoefficientBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.HeckeDetectorCoefficientBounds.annular_norm_le_two line 13
2. lemma OAI.SevenEighths.HeckeDetectorCoefficientBounds.inverseCoefficient_norm_le_two line 17
3. lemma OAI.SevenEighths.HeckeDetectorCoefficientBounds.plainCoefficient_norm_le_two line 30
4. def OAI.SevenEighths.HeckeDetectorCoefficientBounds.expandedSet line 39
5. lemma OAI.SevenEighths.HeckeDetectorCoefficientBounds.expandedSet_count line 41
6. theorem OAI.SevenEighths.HeckeDetectorCoefficientBounds.coefficient_mass line 51