OAI/Combinatorics/EditApproximation/Binary/IntegerBinaryWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.integerBinaryWork line 11

   Source documentation

   Full integer-input runtime with concrete local, setup, and final-output routines.

   noncomputable def integerBinaryWork (source target : List ℤ) (N : ℕ) (epsilon : BinaryFraction) :=
   …

   Mentions: OAI.EditApproximation.BinaryFraction

2. theorem OAI.EditApproximation.integerBinaryWork_expected_near_linear line 17