OAI/Combinatorics/EditApproximation/Geometry/BalancedWidths.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Width and node counts for the fixed interval tree

Repeated ceiling division gives the physical-depth width bound. This includes empty children and repeated interval labels, which must still be counted as distinct nodes in the lazy evaluation analysis.

  1. theorem OAI.EditApproximation.ceilDiv_comp line 17
  2. theorem OAI.EditApproximation.balanced_child_width_le_ceiling line 24
  3. theorem OAI.EditApproximation.sourceChild_width_le_ceiling line 35
  4. theorem OAI.EditApproximation.sourceIntervalAt_width line 42
  5. theorem OAI.EditApproximation.sourceIntervalAt_leaf_width line 54
  6. theorem OAI.EditApproximation.treeLayer_card line 61
  7. theorem OAI.EditApproximation.complete_tree_node_count line 70