OAI/Combinatorics/EditApproximation/Queries/QueryPhysicalInitialCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.querySliceTest_cost line 11

   Source documentation

   The slice test reads only the stored endpoints; it does not materialize the substring.

   theorem querySliceTest_cost {α : Type*} (source : List α) (interval : TargetInterval source.length)
       (B : ℕ) (hB : Nat.size source.length ≤ B) :
       (saturatingSubtractWithWork interval.hi interval.lo).2 +
         (wordLEWithWork (saturatingSubtractWithWork interval.hi interval.lo).1 [true]).2 + 2 ≤ 30 * B + 20 := by
   …

   Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.saturatingSubtractWithWork, OAI.EditApproximation.wordLEWithWork

2. def OAI.EditApproximation.queryPhysicalInitialBitBudget line 23
3. theorem OAI.EditApproximation.queryPhysicalInitial_work_bound line 37
4. theorem OAI.EditApproximation.queryPhysicalInitial_width line 72