OAI/Computability/BinPacking/Trees/CompletionGeometry.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGap.Geometry.Position line 16
  2. def OAI.BinPackingGap.Geometry.theta line 18
  3. def OAI.BinPackingGap.Geometry.heightCode line 21
  4. def OAI.BinPackingGap.Geometry.gap line 24
  5. def OAI.BinPackingGap.Geometry.baseline line 26
  6. def OAI.BinPackingGap.Geometry.beta line 29
  7. def OAI.BinPackingGap.Geometry.lambda line 31
  8. def OAI.BinPackingGap.Geometry.delta line 34
  9. theorem OAI.BinPackingGap.Geometry.base_pos line 36
  10. theorem OAI.BinPackingGap.Geometry.base_one_le line 38
  11. theorem OAI.BinPackingGap.Geometry.widthScale_pos line 42
  12. theorem OAI.BinPackingGap.Geometry.widthScale_one_le line 44
  13. theorem OAI.BinPackingGap.Geometry.gap_pos line 48
  14. theorem OAI.BinPackingGap.Geometry.gap_nonneg line 52
  15. theorem OAI.BinPackingGap.Geometry.gap_le_one_sixteen line 54
  16. theorem OAI.BinPackingGap.Geometry.gap_mul_power line 60
  17. theorem OAI.BinPackingGap.Geometry.theta_nonneg line 65
  18. theorem OAI.BinPackingGap.Geometry.theta_lt_power line 68
  19. theorem OAI.BinPackingGap.Geometry.heightCode_nonneg line 74
  20. theorem OAI.BinPackingGap.Geometry.heightCode_lt_power line 85
  21. theorem OAI.BinPackingGap.Geometry.baseline_lower line 97
  22. theorem OAI.BinPackingGap.Geometry.baseline_upper line 101
  23. theorem OAI.BinPackingGap.Geometry.baseline_range line 107
  24. theorem OAI.BinPackingGap.Geometry.beta_nonneg line 111
  25. theorem OAI.BinPackingGap.Geometry.beta_lt_one_sixteen line 114
  26. theorem OAI.BinPackingGap.Geometry.lambda_pos line 118
  27. theorem OAI.BinPackingGap.Geometry.lambda_nonneg line 121
  28. theorem OAI.BinPackingGap.Geometry.lambda_zero line 124
  29. theorem OAI.BinPackingGap.Geometry.lambda_succ line 127
  30. theorem OAI.BinPackingGap.Geometry.lambda_antitone line 131
  31. theorem OAI.BinPackingGap.Geometry.lambda_le_gap line 136
  32. theorem OAI.BinPackingGap.Geometry.lambda_le_one line 139
  33. theorem OAI.BinPackingGap.Geometry.lambda_lt_tenth line 143
  34. theorem OAI.BinPackingGap.Geometry.lambda_one_le_hundredth line 147
  35. theorem OAI.BinPackingGap.Geometry.delta_pos line 154
  36. theorem OAI.BinPackingGap.Geometry.delta_nonneg line 157
  37. theorem OAI.BinPackingGap.Geometry.delta_le_tenth line 159
  38. theorem OAI.BinPackingGap.Geometry.delta_lt_gap line 163
  39. theorem OAI.BinPackingGap.Geometry.lambda_one_add_two_delta_lt_gap line 169
  40. theorem OAI.BinPackingGap.Geometry.children_succ_lt_parent line 176
  41. theorem OAI.BinPackingGap.Geometry.first_children_lt_gap_twentyfifth line 185
  42. theorem OAI.BinPackingGap.Geometry.first_children_lt_tenth line 195
  43. theorem OAI.BinPackingGap.Geometry.lambda_add_delta_lt_three line 201
  44. def OAI.BinPackingGap.completion line 211
  45. def OAI.BinPackingGap.completionInterval line 214
  46. theorem OAI.BinPackingGap.completion_false line 217
  47. theorem OAI.BinPackingGap.completion_true line 221
  48. theorem OAI.BinPackingGap.baseline_sub_completion line 225
  49. theorem OAI.BinPackingGap.completion_le_baseline line 231
  50. theorem OAI.BinPackingGap.completion_length_nonneg line 236
  51. theorem OAI.BinPackingGap.mem_completionInterval line 242
  52. theorem OAI.BinPackingGap.completion_le_deadline_iff line 247
  53. theorem OAI.BinPackingGap.completion_zero_global_length_le line 254
  54. theorem OAI.BinPackingGap.completion_zero_global_interval_subset line 259
  55. theorem OAI.BinPackingGap.completion_zero_global_bounds line 266
  56. theorem OAI.BinPackingGap.completion_long_zero_lengths line 273
  57. theorem OAI.BinPackingGap.completion_short_zero_lengths line 276
  58. theorem OAI.BinPackingGap.completionInterval_long_zero_lengths line 279
  59. theorem OAI.BinPackingGap.completionInterval_short_zero_lengths line 283
  60. theorem OAI.BinPackingGap.completion_plus_le_one line 287
  61. theorem OAI.BinPackingGap.completion_minus_gt_one line 293
  62. theorem OAI.BinPackingGap.not_mem_plus_completionInterval line 301
  63. theorem OAI.BinPackingGap.not_mem_minus_completionInterval line 307
  64. theorem OAI.BinPackingGap.completion_zero_global_geometry_length_le line 317
  65. theorem OAI.BinPackingGap.completion_minus_geometry_gt_one line 323
  66. theorem OAI.BinPackingGap.completion_job_interval line 331