OAI/Combinatorics/EditApproximation/Refinement/PhysicalIndexedCoarseWork.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.physicalFamilyIndexedCoarseWork_bound line 32

   Source documentation

   Bit arithmetic is executed once for each fresh coarse source request.

   theorem physicalFamilyIndexedCoarseWork_bound (bits : ℕ) (encode : Sum Key Table → ℕ)
       (root : Table) (coarse : PhysicalCoarseDraw source target B depth) (C : ℝ)
       (hc : ∀ entry : PhysicalEntry M J target.length,
         (coarseIndexedEntryBinaryCost N B (depth entry) (physicalSource source entry.1)
           (substring target entry.2.lo entry.2.hi) (coarse entry) : ℝ) ≤
           C * ((coarseInitialArrayWork B (depth entry) (initialThresholdQ N) (initialLambda N)
             (physicalSource source entry.1) (substring target entry.2.lo entry.2.hi) (coarse entry) : ℝ) +
             ((physicalSource source entry.1).length + 1 : ℕ))) :
       physicalFamilyIndexedCoarseWork source target N P H T S passes copies factor multiplier
         tau eta kappa delta draw depth bits encode root coarse ≤ C *
         (physicalFamilyMemoCoarseWork source target N P H T S passes copies factor multiplier
           tau eta kappa delta draw B depth bits encode root coarse +
   …

   Mentions: OAI.EditApproximation.PhysicalCoarseDraw, OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.coarseIndexedEntryBinaryCost, OAI.EditApproximation.physicalSource, OAI.EditApproximation.substring, OAI.EditApproximation.coarseInitialArrayWork, OAI.EditApproximation.initialThresholdQ, OAI.EditApproximation.initialLambda, OAI.EditApproximation.physicalFamilyIndexedCoarseWork, OAI.EditApproximation.physicalFamilyMemoCoarseWork