OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarseArrayStorage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.computedCoarseRootArray_storage line 10
2. theorem OAI.EditApproximation.BinaryFraction.coarseRootArrayStorage_polynomial_scalar line 37
3. theorem OAI.EditApproximation.BinaryFraction.computedCoarseAllRootArrays_storage line 56

   Source documentation

   Even retaining the final array from every candidate uses polynomial space; the implementation may release each array after its root lookup.

   theorem computedCoarseAllRootArrays_storage :
       ∀ᶠ N : ℕ in atTop, ∀ B d : ℕ, ∀ x y : List ℕ,
         B = (integerParameters N).B → d = computedCoarseDepth N (coarseEntryWidth x y) →
         coarseEntryWidth x y ≤ N →
         ∀ (hB : 0 < B) (hq : 0 < inputHeight N ^ 4) (hL : 0 < 64 * inputHeight N)
         (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d),
         (∑ i : CoarseGuessIndex (coarseEntryWidth x y),
           coarseArrayStorage (coarseIndexedRootArray (coarseGuess (coarseEntryWidth x y) i)
             (inputHeight N ^ 4) (64 * inputHeight N) hB hq hL x y (draws i))) ≤
           (N + 2) ^ 25 := by
   …

   Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseArrayStorage, OAI.EditApproximation.BinaryFraction.coarseIndexedRootArray, OAI.EditApproximation.coarseGuess