OAI/NumberTheory/DirichletL/Hecke/DetectorWitnessArithmetic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeDetectorWitnessArithmetic.cutoffCoefficient line 11
2. theorem OAI.SevenEighths.HeckeDetectorWitnessArithmetic.fiber_norm_le line 15
3. theorem OAI.SevenEighths.HeckeDetectorWitnessArithmetic.cutoffCoefficient_small line 21
4. theorem OAI.SevenEighths.HeckeDetectorWitnessArithmetic.cutoffCoefficient_tail line 36
5. theorem OAI.SevenEighths.HeckeDetectorWitnessArithmetic.weighted_fiber line 60
6. def OAI.SevenEighths.HeckeDetectorWitnessArithmetic.exponentialTerm line 74
7. theorem OAI.SevenEighths.HeckeDetectorWitnessArithmetic.exponentialTerm_tail line 78
8. theorem OAI.SevenEighths.HeckeDetectorWitnessArithmetic.exponential_sum_tail line 96