OAI/NumberTheory/DirichletL/Hecke/DetectorWitnessRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.HeckeDetectorWitnessRows.dyadicLength line 10
2. structure OAI.SevenEighths.HeckeDetectorWitnessRows.Witness line 12
3. def OAI.SevenEighths.HeckeDetectorWitnessRows.Witness.frequency line 37
4. theorem OAI.SevenEighths.HeckeDetectorWitnessRows.Witness.frequency_bound line 40
5. theorem OAI.SevenEighths.HeckeDetectorWitnessRows.Witness.real_part_upper line 49
6. theorem OAI.SevenEighths.HeckeDetectorWitnessRows.Witness.left_exponent line 54
7. theorem OAI.SevenEighths.HeckeDetectorWitnessRows.Witness.right_exponent line 59
8. theorem OAI.SevenEighths.HeckeDetectorWitnessRows.exists_from_maximum line 64