OAI/Combinatorics/EditApproximation/Binary/IntegerOccurrenceIndex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform input preparation chooses dictionary widths from the actual integer words. No alphabet size or polynomial exponent is an algorithm input.

  1. theorem OAI.EditApproximation.integerMagnitude_mem line 16
  2. theorem OAI.EditApproximation.integerMagnitude_le line 25
  3. theorem OAI.EditApproximation.integerInputSymbolBits_fits line 36
  4. theorem OAI.EditApproximation.integerInputSymbolBits_le line 42
  5. def OAI.EditApproximation.integerOccurrenceQuery line 49
  6. theorem OAI.EditApproximation.integerOccurrenceQuery_correct line 54
  7. theorem OAI.EditApproximation.integerOccurrenceBuildWithWork_spec line 85
  8. theorem OAI.EditApproximation.integerInputSymbolBits_polynomial line 95

    Source documentation

    Polynomially bounded input words produce logarithmic dictionary keys; the polynomial degree is only an analysis parameter.

    theorem integerInputSymbolBits_polynomial (source target : List ℤ) (N C : ℕ)
    (h : ∀ z ∈ source ++ target, z.natAbs ≤ (N + 2) ^ C) :
    integerInputSymbolBits source target ≤ C * Nat.size (N + 2) + 3 := by
…

    Mentions: OAI.EditApproximation.integerInputSymbolBits

  9. theorem OAI.EditApproximation.integerOccurrenceBuildWithWork_polynomial line 104