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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Terminating rational-ball searches give product names and the scaled physical-time input used by the viscosity-dependent detector evaluator.

  1. def OAI.ForcedComputation.scalarBallReady line 12
  2. instance OAI.ForcedComputation.(instance at line 14) line 14
  3. theorem OAI.ForcedComputation.scalarBallReady_exists line 17
  4. def OAI.ForcedComputation.scalarBallApprox line 24
  5. theorem OAI.ForcedComputation.scalarBallApprox_spec line 27
  6. def OAI.ForcedComputation.mulNameBalls line 33
  7. theorem OAI.ForcedComputation.mulNameBalls_contains line 36
  8. theorem OAI.ForcedComputation.mulNameBalls_converges line 41
  9. def OAI.ForcedComputation.mulFastName line 46
  10. theorem OAI.ForcedComputation.mulFastName_spec line 51
  11. def OAI.ForcedComputation.timeName line 59
  12. theorem OAI.ForcedComputation.timeName_spec line 61
  13. def OAI.ForcedComputation.scaleTimeName line 67
  14. theorem OAI.ForcedComputation.scaleTimeName_spec line 72