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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite pulse slots occupy successive closed cells. The unused half of each cell and the final cell are stationary.

  1. def OAI.ForcedComputation.PlanarTiming.cut line 15
  2. theorem OAI.ForcedComputation.PlanarTiming.cut_zero line 17
  3. theorem OAI.ForcedComputation.PlanarTiming.cut_last line 19
  4. theorem OAI.ForcedComputation.PlanarTiming.cut_mono line 23
  5. theorem OAI.ForcedComputation.PlanarTiming.finish_eq_cut line 26
  6. theorem OAI.ForcedComputation.PlanarTiming.cut_le_start line 31
  7. theorem OAI.ForcedComputation.PlanarTiming.pulse_other_on_cell line 38
  8. theorem OAI.ForcedComputation.PlanarTiming.pulse_on_tail line 50
  9. theorem OAI.ForcedComputation.Recorder.Planar.compiledVelocity_on_cell line 61
  10. theorem OAI.ForcedComputation.Recorder.Planar.compiledVelocity_on_tail line 74