OAI/Combinatorics/EditApproximation/Coarse/CoarseBinaryBox.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.CoarseBinaryBox line 9

   Source documentation

   A zero marker or one full shift array on the execution's common grid.

   def CoarseBinaryBox (two : BinaryFraction) (n V D A : ℕ) (array : CoarseBinaryArray) : Prop :=
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.CoarseBinaryArray

2. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryBox_none line 12
3. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryBox_mono line 16
4. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipAddWithWork_bounds line 22
5. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipAddWithWork_length line 41
6. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryAddWithWork_box line 54
7. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryAddWithWork_cost line 72
8. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyWithWork_box line 87
9. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyWithWork_cost line 103
10. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryMapWithWork_box line 114
11. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryMapWithWork_cost line 131