OAI/Computability/BinPacking/Trees/IntegerTreeGeometry.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGap.UniformTree line 14
  2. def OAI.BinPackingGap.UniformTree.prefixes line 23
  3. theorem OAI.BinPackingGap.UniformTree.mem_prefixes_iff line 26
  4. def OAI.BinPackingGap.UniformTree.vertices line 37
  5. theorem OAI.BinPackingGap.UniformTree.mem_vertices_iff line 40
  6. theorem OAI.BinPackingGap.UniformTree.leaf_mem_vertices line 44
  7. theorem OAI.BinPackingGap.UniformTree.nil_mem_vertices line 48
  8. theorem OAI.BinPackingGap.UniformTree.vertices_nonempty line 52
  9. theorem OAI.BinPackingGap.UniformTree.prefix_mem_vertices line 55
  10. theorem OAI.BinPackingGap.UniformTree.take_mem_vertices line 60
  11. theorem OAI.BinPackingGap.UniformTree.length_le_height line 64
  12. theorem OAI.BinPackingGap.UniformTree.mem_leaves_iff_length_eq_height line 69
  13. abbrev OAI.BinPackingGap.UniformTree.Node line 78
  14. instance OAI.BinPackingGap.UniformTree.nodeFintype line 80
  15. def OAI.BinPackingGap.UniformTree.root line 83
  16. instance OAI.BinPackingGap.UniformTree.nodeNonempty line 85
  17. theorem OAI.BinPackingGap.UniformTree.root_val line 87
  18. theorem OAI.BinPackingGap.UniformTree.node_card line 89
  19. theorem OAI.BinPackingGap.UniformTree.node_card_pos line 92
  20. def OAI.BinPackingGap.UniformTree.depth line 95
  21. def OAI.BinPackingGap.UniformTree.ancestor line 97
  22. def OAI.BinPackingGap.UniformTree.leaf line 99
  23. def OAI.BinPackingGap.UniformTree.child line 101
  24. theorem OAI.BinPackingGap.UniformTree.depth_root line 104
  25. theorem OAI.BinPackingGap.UniformTree.depth_le_height line 106
  26. theorem OAI.BinPackingGap.UniformTree.leaf_iff_depth_eq_height line 109
  27. theorem OAI.BinPackingGap.UniformTree.ancestor_refl line 113
  28. theorem OAI.BinPackingGap.UniformTree.ancestor_trans line 116
  29. theorem OAI.BinPackingGap.UniformTree.ancestor_depth_le line 119
  30. theorem OAI.BinPackingGap.UniformTree.eq_of_ancestor_of_depth_eq line 122
  31. theorem OAI.BinPackingGap.UniformTree.root_ancestor line 126
  32. theorem OAI.BinPackingGap.UniformTree.eq_root_iff_depth_eq_zero line 129
  33. def OAI.BinPackingGap.UniformTree.ancestorAt line 138
  34. theorem OAI.BinPackingGap.UniformTree.ancestorAt_val line 141
  35. theorem OAI.BinPackingGap.UniformTree.ancestorAt_ancestor line 144
  36. theorem OAI.BinPackingGap.UniformTree.depth_ancestorAt line 147
  37. theorem OAI.BinPackingGap.UniformTree.ancestor_eq_ancestorAt line 151
  38. def OAI.BinPackingGap.UniformTree.branchBound line 155
  39. theorem OAI.BinPackingGap.UniformTree.one_le_branchBound line 158
  40. theorem OAI.BinPackingGap.UniformTree.branchBound_pos line 161
  41. theorem OAI.BinPackingGap.UniformTree.label_pos line 164
  42. theorem OAI.BinPackingGap.UniformTree.label_le_branchBound line 169
  43. theorem OAI.BinPackingGap.UniformTree.exists_child_word line 179
  44. theorem OAI.BinPackingGap.UniformTree.exists_child line 193
  45. theorem OAI.BinPackingGap.UniformTree.child_depth line 198
  46. theorem OAI.BinPackingGap.UniformTree.child_ancestor line 203
  47. theorem OAI.BinPackingGap.UniformTree.child_label_bounds line 208
  48. theorem OAI.BinPackingGap.UniformTree.leaf_iff_no_child line 213
  49. def OAI.BinPackingGap.levelCount line 229
  50. def OAI.BinPackingGap.colorCount line 232
  51. theorem OAI.BinPackingGap.colorCount_eq_card_inter_prefixes line 235
  52. def OAI.BinPackingGap.RespectsTreeQuota line 244
  53. structure OAI.BinPackingGap.AuxiliaryTree line 249
  54. theorem OAI.BinPackingGap.card_hit_le line 273
  55. theorem OAI.BinPackingGap.exists_disjoint_of_card_lt line 296
  56. def OAI.BinPackingGap.prefixesAfter line 309
  57. theorem OAI.BinPackingGap.mem_prefixesAfter_iff line 313
  58. theorem OAI.BinPackingGap.stem_not_mem_prefixesAfter line 318
  59. theorem OAI.BinPackingGap.prefixes_append_eq line 326
  60. theorem OAI.BinPackingGap.disjoint_positive_prefixes_cons line 346
  61. theorem OAI.BinPackingGap.disjoint_prefixesAfter_cons line 359
  62. theorem OAI.BinPackingGap.disjoint_positive_spine_prefixes line 370
  63. theorem OAI.BinPackingGap.disjoint_spine_prefixesAfter line 376
  64. inductive OAI.BinPackingGap.TreeGeometry.Side line 388
  65. instance OAI.BinPackingGap.TreeGeometry.(instance at line 393) line 393
  66. def OAI.BinPackingGap.TreeGeometry.rootOffset line 397
  67. def OAI.BinPackingGap.TreeGeometry.pathSum line 401
  68. def OAI.BinPackingGap.TreeGeometry.left line 405
  69. def OAI.BinPackingGap.TreeGeometry.width line 408
  70. def OAI.BinPackingGap.TreeGeometry.right line 411
  71. def OAI.BinPackingGap.TreeGeometry.cell line 414
  72. def OAI.BinPackingGap.TreeGeometry.BoundedAddress line 417
  73. theorem OAI.BinPackingGap.TreeGeometry.boundedAddress_node line 419
  74. theorem OAI.BinPackingGap.TreeGeometry.left_nil line 423
  75. theorem OAI.BinPackingGap.TreeGeometry.width_nil line 426
  76. theorem OAI.BinPackingGap.TreeGeometry.right_nil line 428
  77. theorem OAI.BinPackingGap.TreeGeometry.width_of_ne_nil line 431
  78. theorem OAI.BinPackingGap.TreeGeometry.width_pos line 434
  79. theorem OAI.BinPackingGap.TreeGeometry.left_lt_right line 439
  80. theorem OAI.BinPackingGap.TreeGeometry.cell_nonempty line 443
  81. theorem OAI.BinPackingGap.TreeGeometry.pathSum_append line 447
  82. theorem OAI.BinPackingGap.TreeGeometry.left_append_singleton line 457
  83. theorem OAI.BinPackingGap.TreeGeometry.right_append_singleton line 463
  84. theorem OAI.BinPackingGap.TreeGeometry.child_endpoints line 471
  85. theorem OAI.BinPackingGap.TreeGeometry.append_endpoints line 494
  86. theorem OAI.BinPackingGap.TreeGeometry.prefix_endpoints line 507
  87. theorem OAI.BinPackingGap.TreeGeometry.cell_subset_of_prefix line 513
  88. theorem OAI.BinPackingGap.TreeGeometry.nonroot_endpoints line 520
  89. theorem OAI.BinPackingGap.TreeGeometry.exists_snoc_of_length_succ line 539
  90. theorem OAI.BinPackingGap.TreeGeometry.same_depth_gap line 547
  91. theorem OAI.BinPackingGap.TreeGeometry.eq_of_short_intersections line 600
  92. def OAI.BinPackingGap.TreeGeometry.nodeCell line 616
  93. theorem OAI.BinPackingGap.TreeGeometry.nodeCell_subset_of_ancestor line 619
  94. theorem OAI.BinPackingGap.TreeGeometry.nodeCell_subset_root line 624
  95. theorem OAI.BinPackingGap.TreeGeometry.nonroot_nodeCell_first_tenth line 630
  96. theorem OAI.BinPackingGap.TreeGeometry.mem_ancestor_cell line 640
  97. theorem OAI.BinPackingGap.TreeGeometry.leaf_intersection_is_ancestor line 646
  98. def OAI.BinPackingGap.TreeGeometry.commonBranchBound line 662
  99. theorem OAI.BinPackingGap.TreeGeometry.plus_branch_le line 665
  100. theorem OAI.BinPackingGap.TreeGeometry.minus_branch_le line 668
  101. def OAI.BinPackingGap.IntegerPackingArithmetic.pathNumerator line 675
  102. def OAI.BinPackingGap.IntegerPackingArithmetic.rootOffsetNumerator line 680
  103. def OAI.BinPackingGap.IntegerPackingArithmetic.treeLeftNumerator line 684
  104. def OAI.BinPackingGap.IntegerPackingArithmetic.treeRightNumerator line 688
  105. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_mul_pathSum line 693
  106. theorem OAI.BinPackingGap.IntegerPackingArithmetic.rootOffsetNumerator_cast line 717
  107. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_mul_treeLeft line 721
  108. theorem OAI.BinPackingGap.IntegerPackingArithmetic.geomDenominator_mul_treeRight line 731