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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The finite detector program at a named viscosity. Rational interval products certify every output component, including all time derivatives.

  1. def OAI.ForcedComputation.VelocityDetector.detectorForceName line 15
  2. theorem OAI.ForcedComputation.VelocityDetector.detectorForceName_spec line 19
  3. def OAI.ForcedComputation.VelocityDetector.viscosityForceBalls line 31
  4. theorem OAI.ForcedComputation.VelocityDetector.viscosityForceBalls_contains line 37
  5. theorem OAI.ForcedComputation.VelocityDetector.viscosityForceBalls_converges line 49
  6. def OAI.ForcedComputation.VelocityDetector.evaluateDetectorViscosityForce line 61
  7. theorem OAI.ForcedComputation.VelocityDetector.evaluateDetectorViscosityForce_spec line 69
  8. def OAI.ForcedComputation.VelocityDetector.viscosityBound line 80
  9. theorem OAI.ForcedComputation.VelocityDetector.viscosityBound_ge_one line 82
  10. theorem OAI.ForcedComputation.VelocityDetector.viscosityBound_spec line 86
  11. def OAI.ForcedComputation.VelocityDetector.detectorViscosityBound line 95
  12. theorem OAI.ForcedComputation.VelocityDetector.detectorViscosityBound_spec line 100