OAI/Combinatorics/EditApproximation/Binary/BinaryRepresentativeReads.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Query-local representative construction reads its finite initial table explicitly. Each center lookup is charged before testing it.

  1. def OAI.EditApproximation.BinaryFraction.representativeScalePlainWithWork line 14
  2. theorem OAI.EditApproximation.BinaryFraction.representativeScaleReadWithWork_eq_cost line 26
  3. theorem OAI.EditApproximation.BinaryFraction.localRepresentativeReadWithWork_eq_cost line 46
  4. theorem OAI.EditApproximation.BinaryFraction.localRepresentativeReadWithWork_cost line 68