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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite rational interval arithmetic for vector-valued derivative formulas. The stopping test is rational and finite; convergence proves its termination.

  1. def OAI.ForcedComputation.realNameBall line 13
  2. def OAI.ForcedComputation.vectorNameBall line 16
  3. theorem OAI.ForcedComputation.realNameBall_contains line 19
  4. theorem OAI.ForcedComputation.realNameBall_converges line 23
  5. theorem OAI.ForcedComputation.vectorNameBall_contains line 32
  6. theorem OAI.ForcedComputation.vectorNameBall_converges line 40
  7. def OAI.ForcedComputation.vectorBallReady line 48
  8. instance OAI.ForcedComputation.(instance at line 51) line 51
  9. theorem OAI.ForcedComputation.vectorBallReady_exists line 55
  10. def OAI.ForcedComputation.evaluateVectorBalls line 64
  11. theorem OAI.ForcedComputation.evaluateVectorBalls_spec line 68