OAI/Computability/BinPacking/Trees/TestGeometry.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.Geometry.jobLeft line 11
  2. def OAI.BinPackingGap.Geometry.closedJobCell line 14
  3. def OAI.BinPackingGap.Geometry.jobTestInterval line 17
  4. def OAI.BinPackingGap.Geometry.jobInterior line 20
  5. theorem OAI.BinPackingGap.Geometry.closed_interval_gap_le_length line 23
  6. theorem OAI.BinPackingGap.Geometry.closed_interval_cannot_meet_of_lt_gap line 35
  7. theorem OAI.BinPackingGap.Geometry.jobLeft_lt_baseline line 41
  8. theorem OAI.BinPackingGap.Geometry.one_tenth_lt_jobLeft line 47
  9. theorem OAI.BinPackingGap.Geometry.job_baseline_lt_one line 55
  10. theorem OAI.BinPackingGap.Geometry.closedJobCell_bounds line 60
  11. theorem OAI.BinPackingGap.Geometry.closedJobCell_subset_plusRoot line 65
  12. theorem OAI.BinPackingGap.Geometry.jobTestInterval_subset_closedJobCell line 71
  13. theorem OAI.BinPackingGap.Geometry.job_gap_of_posLT line 76
  14. theorem OAI.BinPackingGap.Geometry.baseline_lt_jobLeft_of_posLT line 82
  15. theorem OAI.BinPackingGap.Geometry.closedJobCell_disjoint line 88
  16. theorem OAI.BinPackingGap.Geometry.jobTestInterval_disjoint line 98
  17. theorem OAI.BinPackingGap.Geometry.closedJobCell_unique_of_short_interval line 106
  18. theorem OAI.BinPackingGap.Geometry.closedJobCell_unique_of_short_halfOpen line 121
  19. theorem OAI.BinPackingGap.Geometry.jobInterior_mem_jobTestInterval line 132
  20. theorem OAI.BinPackingGap.Geometry.jobInterior_mem_closedJobCell line 136
  21. theorem OAI.BinPackingGap.Geometry.baseline_le_jobInterior line 141
  22. theorem OAI.BinPackingGap.Geometry.jobInterior_mem_jobTestInterval_iff line 145
  23. def OAI.BinPackingGap.InventoryData.geometryBound line 155
  24. theorem OAI.BinPackingGap.InventoryData.plus_branch_le_geometryBound line 157
  25. theorem OAI.BinPackingGap.InventoryData.minus_branch_le_geometryBound line 160
  26. def OAI.BinPackingGap.InventoryData.incidencePosition line 163
  27. theorem OAI.BinPackingGap.InventoryData.incidencePosition_injective line 166
  28. def OAI.BinPackingGap.InventoryData.testLeft line 178
  29. def OAI.BinPackingGap.InventoryData.testRight line 185
  30. def OAI.BinPackingGap.InventoryData.testCell line 191
  31. def OAI.BinPackingGap.InventoryData.testInterval line 194
  32. theorem OAI.BinPackingGap.InventoryData.testLeft_lt_testRight line 197
  33. theorem OAI.BinPackingGap.InventoryData.tree_endpoints_in_root line 204
  34. theorem OAI.BinPackingGap.InventoryData.test_endpoints_bounds line 214
  35. theorem OAI.BinPackingGap.InventoryData.testLeft_nonneg line 233
  36. theorem OAI.BinPackingGap.InventoryData.testRight_le_five line 236
  37. theorem OAI.BinPackingGap.InventoryData.testCell_subset_range line 239
  38. theorem OAI.BinPackingGap.InventoryData.testInterval_subset_testCell line 244
  39. theorem OAI.BinPackingGap.InventoryData.disjoint_of_endpoint_lt line 247
  40. theorem OAI.BinPackingGap.InventoryData.same_depth_cells_disjoint line 253
  41. theorem OAI.BinPackingGap.InventoryData.plusLeaf_right_lt_tenth line 266
  42. theorem OAI.BinPackingGap.InventoryData.plusLeaf_job_disjoint line 279
  43. theorem OAI.BinPackingGap.InventoryData.minusLeaf_job_disjoint line 287
  44. theorem OAI.BinPackingGap.InventoryData.testCell_disjoint line 300
  45. theorem OAI.BinPackingGap.InventoryData.testCell_pairwise_disjoint line 346
  46. theorem OAI.BinPackingGap.InventoryData.testInterval_disjoint line 351
  47. theorem OAI.BinPackingGap.InventoryData.testInterval_pairwise_disjoint line 358