OAI/Combinatorics/EditApproximation/Binary/IntegerStoredDataSpace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.natural_pair_storage line 11
2. theorem OAI.EditApproximation.storedNaturalInput_polynomial line 27
3. theorem OAI.EditApproximation.combine_input_storage line 40

   Source documentation

   The explicitly retained original integer input, its encoded arrays, and the target occurrence index.

   private theorem combine_input_storage (X C raw encoded index : ℕ) (hX : 2 ≤ X)
       (hr : raw ≤ X ^ (C + 3)) (he : encoded ≤ X ^ 15) (hi : index ≤ X ^ 6) :
       raw + encoded + index ≤ X ^ (C + 22) := by
   …

4. theorem OAI.EditApproximation.integerStoredDataSpace_polynomial line 53