OAI/Combinatorics/EditApproximation/Geometry/OccurrenceIndex.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A symbol dictionary of cached position tries. The target is enumerated once; interval occurrence queries use two logarithmic prefix counts.

  1. def OAI.EditApproximation.occurrencePrefixCount line 13
  2. def OAI.EditApproximation.occurrenceRangeCount line 17
  3. theorem OAI.EditApproximation.occurrencePrefixCount_sub line 22
  4. theorem OAI.EditApproximation.occurrenceRangeCount_pos line 36
  5. def OAI.EditApproximation.occurrencePrefix line 62
  6. theorem OAI.EditApproximation.occurrenceBuild_prefix line 65
  7. def OAI.EditApproximation.occurrenceQuery line 92
  8. theorem OAI.EditApproximation.occurrenceQuery_build line 96
  9. theorem OAI.EditApproximation.occurrenceBuildWithWork_spec line 108
  10. theorem OAI.EditApproximation.occurrenceQueryWithWork_spec line 123
  11. theorem OAI.EditApproximation.occurrenceQuery_target line 134

    Source documentation

    Converting the input list to its indexed entries is done only during preprocessing. Subsequent queries use endpoints and the dictionary.

    theorem occurrenceQuery_target (symbolBits positionBits : ℕ) (target : List ℕ)
    (hsymbol : ∀ a ∈ target, a < 2 ^ symbolBits) (hposition : target.length ≤ 2 ^ positionBits)
    (a lo hi : ℕ) (ha : a < 2 ^ symbolBits) (hlo : lo ≤ hi) (hhi : hi ≤ target.length) :
    occurrenceQuery (occurrenceBuild symbolBits positionBits target.zipIdx)
      symbolBits positionBits a lo hi = true ↔ a ∈ substring target lo hi := by
…

    Mentions: OAI.EditApproximation.occurrenceQuery, OAI.EditApproximation.occurrenceBuild, OAI.EditApproximation.substring