OAI/Combinatorics/EditApproximation/Binary/BinaryLocalSourceValues.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact local source-port values for arbitrary gathered answer lists. No cost bound on unqueried coordinates enters these identities.

  1. theorem OAI.EditApproximation.sourceDraw_project_cast line 11
  2. theorem OAI.EditApproximation.BinaryFraction.preparedComputedCellSourceWithWork_value line 28
  3. theorem OAI.EditApproximation.BinaryFraction.computedCellSource_cast_value line 39
  4. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleSourceWithWork_value line 53
  5. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceWithWork_value line 67
  6. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsSourceWithWork_semantic_value line 83
  7. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsSourceWithWork_semantic_value line 107