OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/UnitSpatialClock.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The fixed, mean-zero spatial clock. It runs at unit speed throughout the planar computational corridor and is a finite periodic cutoff expression.

  1. def OAI.ForcedComputation.clockRectangle line 14
  2. def OAI.ForcedComputation.unitSpatialClock line 17
  3. theorem OAI.ForcedComputation.unitSpatialClock_smooth line 19
  4. theorem OAI.ForcedComputation.unitSpatialClock_periodic line 22
  5. theorem OAI.ForcedComputation.unitSpatialClock_one line 26
  6. def OAI.ForcedComputation.verticalClock line 36
  7. theorem OAI.ForcedComputation.verticalClock_smooth line 40
  8. theorem OAI.ForcedComputation.verticalClock_divergence line 48
  9. theorem OAI.ForcedComputation.verticalClock_mean_zero line 59
  10. def OAI.ForcedComputation.unitSpatialClockExpr line 66
  11. theorem OAI.ForcedComputation.unitSpatialClockExpr_valid line 68
  12. theorem OAI.ForcedComputation.unitSpatialClockExpr_val line 71