OAI/Combinatorics/EditApproximation/Coarse/CoarseIndexedEntryCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseIndexedEntryBinaryCost_computed_bound line 14

   Source documentation

   Keep the branch dimensions symbolic when forming the finite source sum.

   theorem coarseIndexedEntryBinaryCost_computed_bound :
       ∀ᶠ N : ℕ in Filter.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 : NeZero B) (draw : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d),
         (coarseIndexedEntryBinaryCost N B d x y draw : ℝ) ≤ (inputHeight N : ℝ) ^ 40 *
           ((coarseInitialArrayWork B d (initialThresholdQ N) (initialLambda N) x y draw : ℝ) +
             (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.coarseIndexedEntryBinaryCost, OAI.EditApproximation.coarseInitialArrayWork, OAI.EditApproximation.initialThresholdQ, OAI.EditApproximation.initialLambda

2. theorem OAI.EditApproximation.coarseIndexedEntryCostSum_bound line 31