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

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Effective startup of an autonomous finite field expression. A fixed three-region selector uses a finite transition expression near startup and the autonomous expression on the entire late-time tail.

  1. theorem OAI.ForcedComputation.residual_congr_germ line 15
  2. theorem OAI.ForcedComputation.residual_eventuallyEq line 24
  3. def OAI.ForcedComputation.startupTransition line 29
  4. theorem OAI.ForcedComputation.startupTransition_valid line 31
  5. theorem OAI.ForcedComputation.startupTransition_val line 34
  6. def OAI.ForcedComputation.startupCode line 52
  7. theorem OAI.ForcedComputation.startupCode_valid line 57
  8. theorem OAI.ForcedComputation.startupCode_val line 60
  9. def OAI.ForcedComputation.zeroCode line 69
  10. theorem OAI.ForcedComputation.zeroCode_valid line 71
  11. theorem OAI.ForcedComputation.zeroCode_val line 73
  12. def OAI.ForcedComputation.startupSelectCode line 77
  13. theorem OAI.ForcedComputation.startupSelectCode_valid line 81
  14. theorem OAI.ForcedComputation.startupSelectCode_germ_of_time line 90
  15. theorem OAI.ForcedComputation.startupSelectCode_germ line 123
  16. def OAI.ForcedComputation.evaluateStartupVelocity line 132
  17. theorem OAI.ForcedComputation.evaluateStartupVelocity_spec line 136
  18. def OAI.ForcedComputation.evaluateStartupForce line 145
  19. theorem OAI.ForcedComputation.evaluateStartupForce_spec line 149
  20. def OAI.ForcedComputation.startupVelocityBound line 160
  21. def OAI.ForcedComputation.startupForceBound line 163
  22. theorem OAI.ForcedComputation.startupSelectCode_bound_le line 167
  23. theorem OAI.ForcedComputation.startupSelectCode_forceBound_le line 176
  24. theorem OAI.ForcedComputation.exists_startup_time_approximation line 186
  25. theorem OAI.ForcedComputation.startupVelocityBound_spec line 192
  26. theorem OAI.ForcedComputation.startupForceBound_spec line 202