OAI/NumberTheory/DirichletL/Hecke/ZeroSupremum.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeZeroSupremum.zeroRealParts line 10
  2. def OAI.SevenEighths.HeckeZeroSupremum.zeroSetWithSentinel line 14
  3. def OAI.SevenEighths.HeckeZeroSupremum.beta line 16
  4. theorem OAI.SevenEighths.HeckeZeroSupremum.zeroRealParts_le_one line 18
  5. theorem OAI.SevenEighths.HeckeZeroSupremum.zeroSet_bddAbove line 23
  6. theorem OAI.SevenEighths.HeckeZeroSupremum.zeroSet_nonempty line 30
  7. theorem OAI.SevenEighths.HeckeZeroSupremum.half_le_beta line 33
  8. theorem OAI.SevenEighths.HeckeZeroSupremum.beta_le_one line 36
  9. theorem OAI.SevenEighths.HeckeZeroSupremum.zero_re_le_beta line 43
  10. theorem OAI.SevenEighths.HeckeZeroSupremum.LFunction_ne_zero_of_beta_lt line 48
  11. theorem OAI.SevenEighths.HeckeZeroSupremum.exists_zero_near_beta line 55
  12. theorem OAI.SevenEighths.HeckeZeroSupremum.beta_le_seven_eighths_of_uniform_margin line 64