OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarseHistory.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.computedCoarseRootHistory_bound line 10
2. theorem OAI.EditApproximation.BinaryFraction.computedCoarseRootHistory_polynomial line 39
3. theorem OAI.EditApproximation.BinaryFraction.computedCoarseAllHistories_polynomial line 74

   Source documentation

   Total stored bits of all recursive array results from all guesses. This bound holds for every draw, without a successful-approximation premise.

   theorem computedCoarseAllHistories_polynomial :
       ∀ᶠ 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),
           coarseRootArrayHistory (coarseGuess (coarseEntryWidth x y) i)
             (inputHeight N ^ 4) (64 * inputHeight N) hB hq hL
             (coarseTargetFrame (coarseGuess (coarseEntryWidth x y) i)
               (coarsePadTo (coarseEntryWidth x y) y)) (coarseEntryTree B d x y) (draws i) 0) ≤
           (N + 2) ^ 37 := by
   …

   Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseRootArrayHistory, OAI.EditApproximation.coarseGuess, OAI.EditApproximation.coarseTargetFrame, OAI.EditApproximation.coarsePadTo, OAI.EditApproximation.coarseEntryTree