OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarseInitialWork.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.computedCoarseInitialWithWork_bound line 12

   Source documentation

   All actual initial-estimator branches have the same source-width charging form. In the long-target branch no target scan or root is executed.

   theorem computedCoarseInitialWithWork_bound :
       ∀ᶠ 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),
         (coarseInitialWithWork (inputHeight N ^ 4) (64 * inputHeight N) N hB hq hL x y draws).2 ≤
           inputHeight N ^ 36 * (coarseInitialArrayWork B d (initialThresholdQ N) (initialLambda N)
             x y draws + x.length + 1) := by
   …

   Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseInitialWithWork, OAI.EditApproximation.coarseInitialArrayWork, OAI.EditApproximation.initialThresholdQ, OAI.EditApproximation.initialLambda