OAI/Combinatorics/EditApproximation/Numerics/RationalWideSpatial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Spatial bounds for a literal rational refinement update.

  1. theorem OAI.EditApproximation.rationalMinimum_map_spatial line 11
  2. theorem OAI.EditApproximation.rationalActionValue_spatial line 25
  3. theorem OAI.EditApproximation.rationalBellman_spatial line 38
  4. theorem OAI.EditApproximation.rationalWideStepCone_spatial line 50
  5. theorem OAI.EditApproximation.rationalRefinementUpdate_le_cone line 65
  6. theorem OAI.EditApproximation.rationalRefinementUpdate_div_lower line 71
  7. theorem OAI.EditApproximation.rationalWideStep_spatial line 79