OAI/Combinatorics/EditApproximation/Refinement/PhysicalDenominator.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual returned values have one additional fixed denominator per tree level.

  1. theorem OAI.EditApproximation.rat_den_add_dvd line 12
  2. theorem OAI.EditApproximation.rat_den_min_dvd line 15
  3. theorem OAI.EditApproximation.rat_den_max_dvd line 21
  4. theorem OAI.EditApproximation.rat_den_sum_dvd line 27
  5. theorem OAI.EditApproximation.rationalMinimum_den_dvd line 37
  6. theorem OAI.EditApproximation.rationalActualWideActions_connection_den line 45
  7. theorem OAI.EditApproximation.rationalActionValue_den_dvd line 53
  8. theorem OAI.EditApproximation.stageInitial_den_one line 69
  9. theorem OAI.EditApproximation.rationalPhysicalBellman_den_dvd line 103
  10. theorem OAI.EditApproximation.stageWarmup_den_one line 123
  11. theorem OAI.EditApproximation.rat_inverse_shift_den_dvd line 136
  12. theorem OAI.EditApproximation.rationalRefinementUpdate_den_dvd line 147
  13. theorem OAI.EditApproximation.rationalOnlineMinimum_den_dvd line 160
  14. theorem OAI.EditApproximation.rationalWideStep_den_dvd line 171
  15. theorem OAI.EditApproximation.physicalRefinement_den_dvd line 205