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

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A single loading period followed by the machine's periodic shear program.

  1. def OAI.ForcedComputation.hasTimeCollar line 15
  2. def OAI.ForcedComputation.collarSwitch line 18
  3. theorem OAI.ForcedComputation.collarSwitch_smooth line 25
  4. theorem OAI.ForcedComputation.collarSwitch_before line 34
  5. theorem OAI.ForcedComputation.collarSwitch_after line 45
  6. theorem OAI.ForcedComputation.collarSwitch_periodic line 56
  7. def OAI.ForcedComputation.initializedProgram line 62
  8. theorem OAI.ForcedComputation.loader_collar_zero line 66
  9. theorem OAI.ForcedComputation.loader_started_collar_one line 71
  10. theorem OAI.ForcedComputation.body_collar_one line 78
  11. theorem OAI.ForcedComputation.initializedProgram_before line 83
  12. theorem OAI.ForcedComputation.initializedProgram_loading line 89
  13. theorem OAI.ForcedComputation.initializedProgram_tail line 96
  14. theorem OAI.ForcedComputation.initializedProgram_smooth line 100
  15. theorem OAI.ForcedComputation.initializedProgram_periodic line 107
  16. theorem OAI.ForcedComputation.initializedProgram_bounded line 117