OAI/Combinatorics/EditApproximation/Coarse/CoarseInitialCost.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseInitialWithWork_cost line 10

   Source documentation

   The dyadic wrapper adds only comparisons, a scan, ceiling, and clamp beyond the sum of the actually executed candidate counters.

   theorem coarseInitialWithWork_cost {B d : ℕ} (q L N A S : ℕ)
       (hB : 0 < B) (hq : 0 < q) (hL : 0 < L) (x y : List ℕ)
       (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B d)
       (hA : 2 ≤ A) (hN : Nat.size N ≤ A)
       (hx : Nat.size x.length ≤ A) (hy : Nat.size y.length ≤ A)
       (hs : ∀ a ∈ x ++ y, Nat.size a ≤ S)
       (hc : ∀ i, (coarseCandidateWithWork q L hB hq hL x y i (draws i)).1.width ≤ A) :
       (coarseInitialWithWork q L N hB hq hL x y draws).2 ≤
         ((List.finRange (Nat.clog 2 (coarseEntryWidth x y) + 1)).map
           (fun i => (coarseCandidateWithWork q L hB hq hL x y i (draws i)).2)).sum +
         (x.length + y.length + 1) * (8 * S + 4) +
         10000 * (Nat.clog 2 (coarseEntryWidth x y) + 2) * (A + 2) ^ 2 := by
   …

   Mentions: OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.BinaryFraction.coarseCandidateWithWork, OAI.EditApproximation.BinaryFraction.width, OAI.EditApproximation.BinaryFraction.coarseInitialWithWork