OAI/Combinatorics/EditApproximation/Geometry/WeightedTreeWork.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Summing width-sensitive work over physical levels

At depth d, the product of the number of nodes and their maximum balanced width is at most the source length plus one layer's node count. This is the precise summation used for fresh coarse-entry requests.

  1. theorem OAI.EditApproximation.mul_ceilDiv_le_add line 17
  2. theorem OAI.EditApproximation.layer_width_work line 25
  3. theorem OAI.EditApproximation.interval_tree_width_work line 30