OAI/NumberTheory/DirichletL/Hecke/DetectorRowCountCrossing.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeDetectorRowCount.denominator line 8
  2. def OAI.SevenEighths.HeckeDetectorRowCount.primeWeight line 10
  3. def OAI.SevenEighths.HeckeDetectorRowCount.crossing line 12
  4. def OAI.SevenEighths.HeckeDetectorRowCount.inverseExponent line 14
  5. def OAI.SevenEighths.HeckeDetectorRowCount.plainExponent line 16
  6. def OAI.SevenEighths.HeckeDetectorRowCount.shortExponent line 18
  7. def OAI.SevenEighths.HeckeDetectorRowCount.longExponent line 20
  8. lemma OAI.SevenEighths.HeckeDetectorRowCount.denominator_lower line 22
  9. theorem OAI.SevenEighths.HeckeDetectorRowCount.crossing_bounds line 26
  10. theorem OAI.SevenEighths.HeckeDetectorRowCount.crossing_average line 57
  11. lemma OAI.SevenEighths.HeckeDetectorRowCount.inverse_at_crossing line 65
  12. lemma OAI.SevenEighths.HeckeDetectorRowCount.plain_at_crossing line 72
  13. theorem OAI.SevenEighths.HeckeDetectorRowCount.selected_short_bound line 79
  14. theorem OAI.SevenEighths.HeckeDetectorRowCount.strict_inverse_capacity line 95
  15. lemma OAI.SevenEighths.HeckeDetectorRowCount.plain_capacity_bound line 104
  16. lemma OAI.SevenEighths.HeckeDetectorRowCount.prime_supply_margin line 112
  17. lemma OAI.SevenEighths.HeckeDetectorRowCount.short_ge_base line 114
  18. lemma OAI.SevenEighths.HeckeDetectorRowCount.inverse_capacity_exponent line 121
  19. theorem OAI.SevenEighths.HeckeDetectorRowCount.capacity_loss line 124
  20. theorem OAI.SevenEighths.HeckeDetectorRowCount.plain_capacity_comparison line 140
  21. lemma OAI.SevenEighths.HeckeDetectorRowCount.inverse_zero_capacity line 162
  22. lemma OAI.SevenEighths.HeckeDetectorRowCount.plain_zero_capacity line 167
  23. lemma OAI.SevenEighths.HeckeDetectorRowCount.long_count_bound line 176