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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A computable time cutoff starts the machine-only periodic body. It changes only during the final empty part of the preceding period, so the body is exactly zero before one and exactly periodic from one onward.

  1. def OAI.ForcedComputation.BalancedBody.activationStart line 14
  2. def OAI.ForcedComputation.BalancedBody.activationFinish line 15
  3. theorem OAI.ForcedComputation.BalancedBody.activation_intervals line 17
  4. theorem OAI.ForcedComputation.BalancedBody.finish_le_activationStart line 34
  5. def OAI.ForcedComputation.BalancedBody.bodyLength line 44
  6. def OAI.ForcedComputation.BalancedBody.activation line 47
  7. def OAI.ForcedComputation.BalancedBody.activated line 50
  8. theorem OAI.ForcedComputation.BalancedBody.raw_late_zero line 53
  9. theorem OAI.ForcedComputation.BalancedBody.velocity_late_zero line 77
  10. theorem OAI.ForcedComputation.BalancedBody.activated_before line 83
  11. theorem OAI.ForcedComputation.BalancedBody.activated_tail line 90
  12. theorem OAI.ForcedComputation.BalancedBody.activated_smooth line 98
  13. theorem OAI.ForcedComputation.BalancedBody.activated_support line 102
  14. theorem OAI.ForcedComputation.BalancedBody.activated_bounded line 106