OAI/Combinatorics/FiniteCircle/Parameters.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.StandingPrimes.small_prime line 11
  2. theorem OAI.FiniteCircle.StandingPrimes.period_bound line 19
  3. theorem OAI.FiniteCircle.StandingPrimes.circle_bound line 26
  4. theorem OAI.FiniteCircle.StandingPrimes.log_circle_bound line 34
  5. theorem OAI.FiniteCircle.StandingPrimes.tags_bound line 47
  6. theorem OAI.FiniteCircle.StandingPrimes.tag_card_bound line 55
  7. theorem OAI.FiniteCircle.recursive_length_bound line 60
  8. theorem OAI.FiniteCircle.StandingPrimes.mask_length_bound line 78
  9. theorem OAI.FiniteCircle.StandingPrimes.excluded_length_bound line 89
  10. theorem OAI.FiniteCircle.StandingPrimes.mask_alphabet_bound line 101
  11. theorem OAI.FiniteCircle.StandingPrimes.excluded_alphabet_bound line 120
  12. theorem OAI.FiniteCircle.StandingPrimes.mask_alphabet_ge line 135
  13. theorem OAI.FiniteCircle.StandingPrimes.excluded_alphabet_ge line 150
  14. theorem OAI.FiniteCircle.StandingPrimes.mask_length_pos line 164
  15. theorem OAI.FiniteCircle.StandingPrimes.excluded_length_pos line 177
  16. theorem OAI.FiniteCircle.logarithmic_width_bound line 186
  17. theorem OAI.FiniteCircle.coded_length_cap line 200
  18. theorem OAI.FiniteCircle.StandingPrimes.log_circle_fourth line 208
  19. theorem OAI.FiniteCircle.lower_coefficient_budget line 216
  20. theorem OAI.FiniteCircle.lower_numeric line 274