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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fast names for the internal logarithmic clock and the reciprocal clock speed. These are operations on rational names, rather than real oracles.

  1. def OAI.ForcedComputation.shiftedTimeName line 12
  2. theorem OAI.ForcedComputation.shiftedTimeName_spec line 14
  3. def OAI.ForcedComputation.clockPointName line 21
  4. theorem OAI.ForcedComputation.clockPointName_spec line 25
  5. def OAI.ForcedComputation.reciprocalClockName line 38
  6. theorem OAI.ForcedComputation.reciprocalClockName_spec line 41