OAI/Combinatorics/EditApproximation/Numerics/RationalRefinement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Rational execution of the Bellman and refinement operations

Every finite minimum, cone cost, warmup iteration, and refinement update is computed in rational arithmetic. The real analysis used elsewhere is the exact cast of these operations. An absent online candidate returns the cone minimum, avoiding an extended-real value in the implementation.

  1. theorem OAI.EditApproximation.rationalMinimum_cast line 21
  2. def OAI.EditApproximation.RationalBellmanAction.toReal line 30
  3. theorem OAI.EditApproximation.rationalActionValue_cast line 38
  4. theorem OAI.EditApproximation.rationalBellman_cast line 47
  5. def OAI.EditApproximation.rationalWarmup line 57
  6. theorem OAI.EditApproximation.rationalWarmup_cast line 62
  7. theorem OAI.EditApproximation.rationalRefinementUpdate_cast line 78
  8. theorem OAI.EditApproximation.rationalRefinementUpdate_none line 84