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

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Rational disjoint pulse slots for a finite planar instruction list.

  1. def OAI.ForcedComputation.PlanarTiming.start line 14
  2. def OAI.ForcedComputation.PlanarTiming.finish line 16
  3. theorem OAI.ForcedComputation.PlanarTiming.intervals line 18
  4. theorem OAI.ForcedComputation.PlanarTiming.ordered line 28
  5. def OAI.ForcedComputation.PlanarTiming.clock line 34
  6. def OAI.ForcedComputation.PlanarTiming.pulse line 36
  7. theorem OAI.ForcedComputation.PlanarTiming.clock_smooth line 38
  8. theorem OAI.ForcedComputation.PlanarTiming.pulse_smooth line 40
  9. theorem OAI.ForcedComputation.PlanarTiming.clock_derivative line 42
  10. theorem OAI.ForcedComputation.PlanarTiming.clock_range line 45
  11. theorem OAI.ForcedComputation.PlanarTiming.clock_at_zero line 48
  12. theorem OAI.ForcedComputation.PlanarTiming.clock_at_one line 52
  13. theorem OAI.ForcedComputation.PlanarTiming.pulse_active line 56
  14. theorem OAI.ForcedComputation.PlanarTiming.active_previous line 62
  15. theorem OAI.ForcedComputation.PlanarTiming.active_future line 69
  16. theorem OAI.ForcedComputation.PlanarTiming.pulse_unique line 76