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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A terminating rational evaluation procedure for every finite moving gate expression and all of its formal mixed derivatives.

  1. def OAI.ForcedComputation.NonperiodicExpr.enclose line 13
  2. theorem OAI.ForcedComputation.NonperiodicExpr.enclose_contains line 20
  3. theorem OAI.ForcedComputation.NonperiodicExpr.enclose_converges line 30
  4. def OAI.ForcedComputation.NonperiodicExpr.Ready line 40
  5. instance OAI.ForcedComputation.NonperiodicExpr.(instance at line 43) line 43
  6. theorem OAI.ForcedComputation.NonperiodicExpr.ready_exists line 46
  7. def OAI.ForcedComputation.NonperiodicExpr.evaluateRational line 52
  8. theorem OAI.ForcedComputation.NonperiodicExpr.evaluateRational_spec line 55