OAI/Combinatorics/EditApproximation/Queries/QueryRefinementFinish.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The final local continuation consumes the two gathered data buffers. It recomputes the local representative list with counted initial reads and runs the Boolean Bellman/online minima on the already selected actions.

  1. theorem OAI.EditApproximation.BinaryFraction.queryRefinementFinishWithWork_value line 26
  2. theorem OAI.EditApproximation.BinaryFraction.queryRefinementFinishWithWork_value_only line 54