OAI/Computability/StarHeight/Markers.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.LocalMarkers.Period line 14
  2. def OAI.GeneralizedStarHeight.LocalMarkers.Aperiodic line 17
  3. def OAI.GeneralizedStarHeight.LocalMarkers.Occurs line 20
  4. def OAI.GeneralizedStarHeight.LocalMarkers.markers line 23
  5. lemma OAI.GeneralizedStarHeight.LocalMarkers.overlap_period line 28
  6. lemma OAI.GeneralizedStarHeight.LocalMarkers.occurrence_separated line 36
  7. lemma OAI.GeneralizedStarHeight.LocalMarkers.separated line 51
  8. lemma OAI.GeneralizedStarHeight.LocalMarkers.occurrence_near line 65
  9. def OAI.GeneralizedStarHeight.LocalMarkers.radius line 83
  10. lemma OAI.GeneralizedStarHeight.LocalMarkers.radius_ge line 85
  11. lemma OAI.GeneralizedStarHeight.LocalMarkers.locality line 90
  12. lemma OAI.GeneralizedStarHeight.LocalMarkers.translate line 121
  13. def OAI.GeneralizedStarHeight.LocalMarkers.priorityList line 144
  14. lemma OAI.GeneralizedStarHeight.LocalMarkers.mem_priorityList line 148
  15. theorem OAI.GeneralizedStarHeight.LocalMarkers.exists_markers line 153
  16. lemma OAI.GeneralizedStarHeight.LocalMarkers.periodic_remainder line 185
  17. lemma OAI.GeneralizedStarHeight.LocalMarkers.periodic_agree line 195
  18. lemma OAI.GeneralizedStarHeight.LocalMarkers.period_mod line 207
  19. def OAI.GeneralizedStarHeight.LocalMarkers.continuation line 231
  20. lemma OAI.GeneralizedStarHeight.LocalMarkers.continuation_periodic line 239
  21. lemma OAI.GeneralizedStarHeight.LocalMarkers.continuation_agrees line 248
  22. lemma OAI.GeneralizedStarHeight.LocalMarkers.exists_continuation line 257
  23. lemma OAI.GeneralizedStarHeight.LocalMarkers.continuation_unique line 263
  24. lemma OAI.GeneralizedStarHeight.FiniteMonoidPeriod.pow_add_of_repeat line 283
  25. lemma OAI.GeneralizedStarHeight.FiniteMonoidPeriod.pow_add_multiple line 288
  26. lemma OAI.GeneralizedStarHeight.FiniteMonoidPeriod.exists_repeat line 296
  27. theorem OAI.GeneralizedStarHeight.FiniteMonoidPeriod.pow_factorial line 310