OAI/Computability/StarHeight/RobustClock.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.RobustClock.vertices line 22
  2. def OAI.GeneralizedStarHeight.RobustClock.FreshPairs line 26
  3. lemma OAI.GeneralizedStarHeight.RobustClock.mem_vertices line 30
  4. lemma OAI.GeneralizedStarHeight.RobustClock.card_vertices line 40
  5. lemma OAI.GeneralizedStarHeight.RobustClock.FreshPairs.nodup line 49
  6. lemma OAI.GeneralizedStarHeight.RobustClock.FreshPairs.realize line 58
  7. lemma OAI.GeneralizedStarHeight.RobustClock.realize_sequence line 88
  8. lemma OAI.GeneralizedStarHeight.RobustClock.extract_forest line 97
  9. lemma OAI.GeneralizedStarHeight.RobustClock.count_of_no_forest line 129
  10. abbrev OAI.GeneralizedStarHeight.RobustClock.Circle line 137
  11. lemma OAI.GeneralizedStarHeight.RobustClock.coe_integer line 139
  12. lemma OAI.GeneralizedStarHeight.RobustClock.representative line 143
  13. lemma OAI.GeneralizedStarHeight.RobustClock.norm_coe_le_abs line 150
  14. lemma OAI.GeneralizedStarHeight.RobustClock.coe_mod_fraction line 153
  15. lemma OAI.GeneralizedStarHeight.RobustClock.grid_near line 164
  16. def OAI.GeneralizedStarHeight.RobustClock.Near line 190
  17. def OAI.GeneralizedStarHeight.RobustClock.centersI line 193
  18. def OAI.GeneralizedStarHeight.RobustClock.centersJ line 196
  19. lemma OAI.GeneralizedStarHeight.RobustClock.center_separation line 199
  20. lemma OAI.GeneralizedStarHeight.RobustClock.center_sums line 205
  21. lemma OAI.GeneralizedStarHeight.RobustClock.type_one_difference line 227
  22. lemma OAI.GeneralizedStarHeight.RobustClock.type_one_interior line 237
  23. def OAI.GeneralizedStarHeight.RobustClock.smallCoords line 271
  24. lemma OAI.GeneralizedStarHeight.RobustClock.mem_smallCoords line 275
  25. def OAI.GeneralizedStarHeight.RobustClock.TypeTwo line 280
  26. lemma OAI.GeneralizedStarHeight.RobustClock.type_two_difference line 283
  27. lemma OAI.GeneralizedStarHeight.RobustClock.type_two_interior line 302
  28. def OAI.GeneralizedStarHeight.RobustClock.FirstI line 349
  29. def OAI.GeneralizedStarHeight.RobustClock.FirstJ line 352
  30. lemma OAI.GeneralizedStarHeight.RobustClock.first_left_right line 355
  31. lemma OAI.GeneralizedStarHeight.RobustClock.first_same_side line 361
  32. lemma OAI.GeneralizedStarHeight.RobustClock.first_interior line 373
  33. lemma OAI.GeneralizedStarHeight.RobustClock.pow_two_half line 392
  34. lemma OAI.GeneralizedStarHeight.RobustClock.pow_two_pos_diff_inj line 397
  35. lemma OAI.GeneralizedStarHeight.RobustClock.pow_two_diff_ne_zero line 414
  36. lemma OAI.GeneralizedStarHeight.RobustClock.pow_two_diff_inj line 419
  37. def OAI.GeneralizedStarHeight.RobustClock.realRoster line 437
  38. lemma OAI.GeneralizedStarHeight.RobustClock.realRoster_range line 441
  39. lemma OAI.GeneralizedStarHeight.RobustClock.realRoster_diff_ne_zero line 450
  40. lemma OAI.GeneralizedStarHeight.RobustClock.realRoster_diff_inj line 461
  41. def OAI.GeneralizedStarHeight.RobustClock.firstRoster line 472
  42. lemma OAI.GeneralizedStarHeight.RobustClock.realRoster_diff_range line 475
  43. lemma OAI.GeneralizedStarHeight.RobustClock.firstRoster_diff_ne_zero line 482
  44. lemma OAI.GeneralizedStarHeight.RobustClock.firstRoster_diff_inj line 493
  45. lemma OAI.GeneralizedStarHeight.RobustClock.finite_positive_lower line 501
  46. def OAI.GeneralizedStarHeight.RobustClock.OffPair line 518
  47. instance OAI.GeneralizedStarHeight.RobustClock.(instance at line 520) line 520
  48. lemma OAI.GeneralizedStarHeight.RobustClock.firstRoster_parameters line 526
  49. lemma OAI.GeneralizedStarHeight.RobustClock.norm_difference_perturb line 566
  50. lemma OAI.GeneralizedStarHeight.RobustClock.first_roster_separation line 573
  51. lemma OAI.GeneralizedStarHeight.RobustClock.first_obstruction_count line 586
  52. def OAI.GeneralizedStarHeight.RobustClock.Forest line 603
  53. instance OAI.GeneralizedStarHeight.RobustClock.(instance at line 606) line 606
  54. def OAI.GeneralizedStarHeight.RobustClock.Batch line 611
  55. instance OAI.GeneralizedStarHeight.RobustClock.(instance at line 613) line 613
  56. lemma OAI.GeneralizedStarHeight.RobustClock.batch_card line 617
  57. def OAI.GeneralizedStarHeight.RobustClock.forestRoster line 621
  58. lemma OAI.GeneralizedStarHeight.RobustClock.forestRoster_spec line 624
  59. def OAI.GeneralizedStarHeight.RobustClock.batchRoster line 628
  60. lemma OAI.GeneralizedStarHeight.RobustClock.batch_forest_hit line 632
  61. lemma OAI.GeneralizedStarHeight.RobustClock.batch_obstruction_count line 659
  62. def OAI.GeneralizedStarHeight.RobustClock.BlockI line 676
  63. def OAI.GeneralizedStarHeight.RobustClock.BlockJ line 679
  64. lemma OAI.GeneralizedStarHeight.RobustClock.block_reversal_false line 682
  65. lemma OAI.GeneralizedStarHeight.RobustClock.block_interior line 705
  66. def OAI.GeneralizedStarHeight.RobustClock.ClockI line 720
  67. def OAI.GeneralizedStarHeight.RobustClock.ClockJ line 725
  68. def OAI.GeneralizedStarHeight.RobustClock.Obstruction line 730
  69. def OAI.GeneralizedStarHeight.RobustClock.Edge line 734
  70. lemma OAI.GeneralizedStarHeight.RobustClock.unequal_edge_unique line 738
  71. lemma OAI.GeneralizedStarHeight.RobustClock.graph_alternative line 781
  72. lemma OAI.GeneralizedStarHeight.RobustClock.clock_interior line 800
  73. lemma OAI.GeneralizedStarHeight.RobustClock.clock_ball line 837
  74. def OAI.GeneralizedStarHeight.RobustClock.roster line 855
  75. def OAI.GeneralizedStarHeight.RobustClock.obstructionPairs line 858
  76. lemma OAI.GeneralizedStarHeight.RobustClock.roster_estimate line 863
  77. def OAI.GeneralizedStarHeight.RobustClock.badPairs line 902
  78. structure OAI.GeneralizedStarHeight.RobustClock.Specification line 907
  79. abbrev OAI.GeneralizedStarHeight.RobustClock.Coordinates line 926
  80. theorem OAI.GeneralizedStarHeight.RobustClock.exists_clock line 930
  81. lemma OAI.GeneralizedStarHeight.RobustClock.Specification.diagonal line 974