OAI/Combinatorics/EditApproximation/Geometry/TreeParameters.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Depth of the computed interval tree

The branching factor is the power of two prescribed by the algorithm. Ceiling logarithms count physical levels, including empty intervals.

  1. theorem OAI.EditApproximation.intervalTreeDepth_capacity line 21
  2. theorem OAI.EditApproximation.intervalTreeDepth_power_le line 25
  3. theorem OAI.EditApproximation.computed_branching_bounds line 41
  4. theorem OAI.EditApproximation.computed_tree_depth_bound line 56
  5. theorem OAI.EditApproximation.computed_source_leaf_width line 79
  6. theorem OAI.EditApproximation.intervalTreeDepth_node_count line 89