OAI/Combinatorics/EditApproximation/Binary/IntegerOccurrenceStorage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.integerOccurrenceStorage_bound line 14

   Source documentation

   Actual counters and trie nodes of the encoded target occurrence index.

   theorem integerOccurrenceStorage_bound (source target : List ℤ) (N C : ℕ)
       (hsize : source.length + target.length ≤ N)
       (hsymbol : ∀ z ∈ source ++ target, z.natAbs ≤ (N + 2) ^ C) :
       integerOccurrenceStorage source target ≤ 9 * (C + 2) * (N + 2) ^ 5 := by
   …

   Mentions: OAI.EditApproximation.integerOccurrenceStorage

2. theorem OAI.EditApproximation.integerOccurrenceStorage_polynomial line 49