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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Certified calls to the input-field oracle at clocked points. The adaptive searches below stop because the input's rational enclosures converge. No evaluator for the output force is assumed.

  1. def OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.modulus line 18
  2. theorem OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.modulus_nonneg line 21
  3. theorem OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.fderiv_bound line 24
  4. theorem OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.lipschitz line 46
  5. def OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.Ready line 56
  6. instance OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.readyDecidable line 59
  7. theorem OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.ready_exists line 63
  8. def OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.evaluate line 69
  9. theorem OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.evaluate_spec line 73
  10. def OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.clockBall line 79
  11. theorem OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.clockBall_contains line 85
  12. theorem OAI.ForcedComputation.VelocityDetector.PlanarJetOracle.clockBall_converges line 112
  13. def OAI.ForcedComputation.VelocityDetector.DetectorExpr.enclose line 124
  14. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.enclose_contains line 131
  15. theorem OAI.ForcedComputation.VelocityDetector.DetectorExpr.enclose_converges line 140