OAI/Combinatorics/EditApproximation/Geometry/OccurrenceLeaf.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Constant-size leaf descriptors use the preprocessed occurrence index. The target interval is represented by endpoints; it is never copied or scanned while evaluating a singleton leaf.

  1. def OAI.EditApproximation.indexedSingletonCost line 13
  2. theorem OAI.EditApproximation.indexedSingletonCost_eq line 18
  3. theorem OAI.EditApproximation.indexedSingletonCostWithWork_spec line 32
  4. def OAI.EditApproximation.indexedLeafCost line 45
  5. theorem OAI.EditApproximation.indexedLeafCost_eq line 51
  6. theorem OAI.EditApproximation.indexedLeafCost_exact line 63