OAI/Combinatorics/EditApproximation/Geometry/OccurrencePrefix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Cached binary position counts. Inserting a position and counting positions strictly below a boundary both follow one root-to-leaf path. Counts are stored at internal nodes, so a prefixCount query does not traverse a whole interval.

  1. theorem OAI.EditApproximation.PositionCounts.count_add line 25
  2. def OAI.EditApproximation.PositionCounts.prefixCount line 33
  3. theorem OAI.EditApproximation.PositionCounts.prefix_empty line 39
  4. theorem OAI.EditApproximation.PositionCounts.prefix_add line 47

    Source documentation

    Adding one stored position changes a prefixCount count by exactly its membership indicator. This holds for any prior tree, without a balance or density assumption.

    theorem prefix_add (tree : PositionCounts) (d i t : ℕ) (hi : i < 2 ^ d) :
    (tree.add d i).prefixCount d t = tree.prefixCount d t + if i < t then 1 else 0 := by
…

    Mentions: OAI.EditApproximation.PositionCounts, OAI.EditApproximation.PositionCounts.prefixCount

  5. theorem OAI.EditApproximation.PositionCounts.addWithWork_spec line 75
  6. theorem OAI.EditApproximation.PositionCounts.prefixWithWork_spec line 85
  7. def OAI.EditApproximation.PositionCounts.nodes line 93
  8. theorem OAI.EditApproximation.PositionCounts.children_nodes line 97
  9. theorem OAI.EditApproximation.PositionCounts.add_nodes line 101