OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarsePolynomial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.computedCoarseBranching_polynomial line 11
2. theorem OAI.EditApproximation.BinaryFraction.computedCoarseInitialArrayWork_polynomial line 22

   Source documentation

   A deterministic bound holds for every pruning outcome, including the outcomes outside the accuracy event.

   theorem computedCoarseInitialArrayWork_polynomial (N B d : ℕ) (x y : List ℕ)
       (hN : 0 < N) (hell : 200 ≤ inputSmallLog N)
       (hBdef : B = (integerParameters N).B)
       (hddef : d = computedCoarseDepth N (coarseEntryWidth x y))
       (hsize : coarseEntryWidth x y ≤ N)
       (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d) :
       coarseInitialArrayWork B d (initialThresholdQ N) (initialLambda N) x y draws ≤
         (N + 2) ^ 19 := by
   …

   Mentions: OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseInitialArrayWork, OAI.EditApproximation.initialThresholdQ, OAI.EditApproximation.initialLambda

3. theorem OAI.EditApproximation.BinaryFraction.computedCoarseIndexedInitialWithWork_polynomial line 68

   Source documentation

   The counted indexed implementation has polynomial work on every draw.

   theorem computedCoarseIndexedInitialWithWork_polynomial :
       ∀ᶠ N : ℕ in atTop, ∀ B d : ℕ, ∀ x y : List ℕ,
         B = (integerParameters N).B → d = computedCoarseDepth N (coarseEntryWidth x y) →
         coarseEntryWidth x y ≤ N → (∀ a ∈ x ++ y, Nat.size a ≤ inputHeight N ^ 3) →
         ∀ (hB : 0 < B) (hq : 0 < inputHeight N ^ 4) (hL : 0 < 64 * inputHeight N)
         (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d),
         (coarseIndexedInitialWithWork (inputHeight N ^ 4) (64 * inputHeight N) N
           hB hq hL x y draws).2 ≤ (N + 2) ^ 180 := by
   …

   Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseIndexedInitialWithWork