OAI/Combinatorics/EditApproximation/Binary/IntegerInputStorage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.storedIntegerBits_le line 14

   Source documentation

   A sign field, magnitude bits and one pointer/header word per input symbol.

   theorem storedIntegerBits_le (values : List ℤ) (A : ℕ)
       (h : ∀ z ∈ values, z.natAbs ≤ A) :
       storedIntegerBits values ≤ 1 + values.length * (A + 2) := by
   …

   Mentions: OAI.EditApproximation.storedIntegerBits

2. theorem OAI.EditApproximation.pair_storage_power line 28
3. theorem OAI.EditApproximation.storedIntegerInput_polynomial line 41