OAI/Combinatorics/EditApproximation/Numerics/RationalPruning.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact candidate pruning uses value lower bounds, without an accuracy event.

  1. theorem OAI.EditApproximation.rationalMinimum_filter_map line 11
  2. theorem OAI.EditApproximation.rationalMinimum_local_complete line 30
  3. theorem OAI.EditApproximation.rationalMinimum_min_fallback line 49
  4. theorem OAI.EditApproximation.rationalMinimum_local_complete_lt line 57
  5. theorem OAI.EditApproximation.rationalMinimum_cons_fallback line 76
  6. theorem OAI.EditApproximation.rationalMinimum_map_max line 81
  7. theorem OAI.EditApproximation.rationalRefinementUpdate_online_list line 89
  8. theorem OAI.EditApproximation.rationalRefinementUpdate_filter_online line 98
  9. theorem OAI.EditApproximation.rationalActionValue_pruned_lower line 108
  10. theorem OAI.EditApproximation.rationalBellman_prune_centers line 120