OAI/Combinatorics/EditApproximation/Coarse/CoarseReadLeafWork.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseLetterMatchWithWork_value line 13

   Source documentation

   Compare one tagged source letter with a framed target lookup.

   theorem coarseLetterMatchWithWork_value (actual : Option (Option ℕ)) (wanted : Option ℕ) :
       (coarseLetterMatchWithWork actual wanted).1 = true ↔ actual = some wanted := by
   …

   Mentions: OAI.EditApproximation.coarseLetterMatchWithWork

2. theorem OAI.EditApproximation.coarseLetterMatchWithWork_cost line 22
3. theorem OAI.EditApproximation.coarseFramedRead_symbol_mem line 36
4. theorem OAI.EditApproximation.BinaryFraction.coarseReadShiftWithWork_value line 48

   Source documentation

   The leaf lookup explicitly adds the shift, reads the indexed frame and compares the stored symbol bits.

   theorem coarseReadShiftWithWork_value (k n : ℕ) (target : List ℕ)
       (letter : Option (Option ℕ)) (start : ℕ) (shift : Fin (2 * k + 1)) :
       (coarseReadShiftWithWork k n target letter start shift).1 =
         coarseReadShiftCost k n target letter start shift := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction.coarseReadShiftWithWork, OAI.EditApproximation.BinaryFraction.coarseReadShiftCost

5. theorem OAI.EditApproximation.BinaryFraction.coarseReadShiftWithWork_cost line 59