OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/ClockedRationalEvaluation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite rational evaluation of a clocked expression, with an adaptive search justified by convergence of its explicit rational enclosures.

  1. def OAI.ForcedComputation.ClockedExpr.enclose line 12
  2. theorem OAI.ForcedComputation.ClockedExpr.enclose_contains line 19
  3. theorem OAI.ForcedComputation.ClockedExpr.enclose_converges line 28
  4. def OAI.ForcedComputation.ClockedExpr.Ready line 37
  5. instance OAI.ForcedComputation.ClockedExpr.(instance at line 40) line 40
  6. theorem OAI.ForcedComputation.ClockedExpr.ready_exists line 44
  7. def OAI.ForcedComputation.ClockedExpr.evaluateRational line 50
  8. theorem OAI.ForcedComputation.ClockedExpr.evaluateRational_spec line 54