OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/CompactDetectorEvaluation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A terminating evaluator for the finite relative detector expressions. It works at arbitrary fast-named spacetime points and for all ordered mixed derivatives. The only oracle calls evaluate derivatives of the input V.

  1. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.Ready line 16
  2. instance OAI.ForcedComputation.VelocityDetector.DetectorExpr.readyDecidable line 20
  3. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.ready_exists line 24
  4. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.evaluateRational line 31
  5. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.evaluateRational_spec line 36
  6. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.derivativeBound line 42
  7. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.derivativeBound_nonneg line 45
  8. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.fderiv_bound line 49
  9. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.lipschitz_bound line 74
  10. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.inputPrecision line 87
  11. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.inputPrecision_spec line 90
  12. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.evaluate line 107
  13. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.evaluate_spec line 113
  14. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.evaluate_mixed_spec line 133