OAI/NumberTheory/DirichletL/Hecke/DetectorZeros.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeDetectorZeros.rectangle line 13
  2. theorem OAI.SevenEighths.HeckeDetectorZeros.rectangle_compact line 16
  3. def OAI.SevenEighths.HeckeDetectorZeros.zeros line 24
  4. theorem OAI.SevenEighths.HeckeDetectorZeros.zeros_finite line 26
  5. def OAI.SevenEighths.HeckeDetectorZeros.zeroFinset line 39
  6. theorem OAI.SevenEighths.HeckeDetectorZeros.mem_zeroFinset line 42
  7. def OAI.SevenEighths.HeckeDetectorZeros.familyZeros line 50
  8. theorem OAI.SevenEighths.HeckeDetectorZeros.mem_familyZeros line 54
  9. def OAI.SevenEighths.HeckeDetectorZeros.realParts line 60
  10. theorem OAI.SevenEighths.HeckeDetectorZeros.realParts_nonempty line 63
  11. def OAI.SevenEighths.HeckeDetectorZeros.zeroMaximum line 66
  12. theorem OAI.SevenEighths.HeckeDetectorZeros.zeroMaximum_mem line 69
  13. theorem OAI.SevenEighths.HeckeDetectorZeros.zeroMaximum_bounds line 72
  14. theorem OAI.SevenEighths.HeckeDetectorZeros.zero_re_le_maximum line 83
  15. theorem OAI.SevenEighths.HeckeDetectorZeros.maximum_attained line 93
  16. theorem OAI.SevenEighths.HeckeDetectorZeros.zeroMaximum_mono line 103
  17. theorem OAI.SevenEighths.HeckeDetectorZeros.nonzero_on_buffered_disk line 113
  18. theorem OAI.SevenEighths.HeckeDetectorZeros.exists_actual_buffered_bin line 134