OAI/Computability/StarHeight/ClockResidues.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.SlotResidues.modulus line 12
  2. def OAI.GeneralizedStarHeight.SlotResidues.representative line 14
  3. lemma OAI.GeneralizedStarHeight.SlotResidues.representative_strict line 16
  4. lemma OAI.GeneralizedStarHeight.SlotResidues.positive_quotient line 22
  5. lemma OAI.GeneralizedStarHeight.SlotResidues.positive_unique line 31
  6. lemma OAI.GeneralizedStarHeight.SlotResidues.signed_unique line 47
  7. lemma OAI.GeneralizedStarHeight.SlotResidues.representative_bounds line 68
  8. lemma OAI.GeneralizedStarHeight.SlotResidues.mod_difference_eq line 82
  9. lemma OAI.GeneralizedStarHeight.SlotResidues.distinct_differences line 100
  10. lemma OAI.GeneralizedStarHeight.SlotResidues.nonzero_difference line 109
  11. lemma OAI.GeneralizedStarHeight.PeriodicClock.large_primes line 131
  12. def OAI.GeneralizedStarHeight.PeriodicClock.speedMap line 144
  13. lemma OAI.GeneralizedStarHeight.PeriodicClock.speedMap_apply line 150
  14. lemma OAI.GeneralizedStarHeight.PeriodicClock.period line 153
  15. lemma OAI.GeneralizedStarHeight.PeriodicClock.crt_grid line 168
  16. lemma OAI.GeneralizedStarHeight.PeriodicClock.net line 189
  17. lemma OAI.GeneralizedStarHeight.ScheduleCopies.exists_log_linear line 219
  18. lemma OAI.GeneralizedStarHeight.ScheduleCopies.exists_log_polynomial line 238
  19. lemma OAI.GeneralizedStarHeight.PeriodicClock.floor_approx line 264
  20. lemma OAI.GeneralizedStarHeight.PeriodicClock.approximate_speeds line 287
  21. lemma OAI.GeneralizedStarHeight.PeriodicClock.dist_coordinate_le line 303
  22. lemma OAI.GeneralizedStarHeight.PeriodicClock.approximate_finite line 308
  23. lemma OAI.GeneralizedStarHeight.PeriodicClock.coprime_product_of_small line 332
  24. lemma OAI.GeneralizedStarHeight.SpacedStencil.exists_points line 348
  25. lemma OAI.GeneralizedStarHeight.SpacedStencil.positive_gap line 384
  26. lemma OAI.GeneralizedStarHeight.SpacedStencil.positive_differences line 391
  27. lemma OAI.GeneralizedStarHeight.SpacedStencil.ordered_differences line 413
  28. lemma OAI.GeneralizedStarHeight.SpacedStencil.nonzero_differences line 434