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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Vector-valued finite clocked programs, with certified evaluation and bounds for every ordered mixed derivative on finite time slabs.

  1. abbrev OAI.ForcedComputation.ClockedVector line 13
  2. def OAI.ForcedComputation.ClockedVector.Valid line 17
  3. def OAI.ForcedComputation.ClockedVector.val line 19
  4. def OAI.ForcedComputation.ClockedVector.diffWord line 21
  5. theorem OAI.ForcedComputation.ClockedVector.valid_diffWord line 24
  6. theorem OAI.ForcedComputation.ClockedVector.smooth line 27
  7. theorem OAI.ForcedComputation.ClockedVector.val_diffWord line 30
  8. def OAI.ForcedComputation.ClockedVector.bound line 45
  9. theorem OAI.ForcedComputation.ClockedVector.bound_nonneg line 48
  10. theorem OAI.ForcedComputation.ClockedVector.val_bound line 52
  11. def OAI.ForcedComputation.ClockedVector.evaluate line 63
  12. theorem OAI.ForcedComputation.ClockedVector.evaluate_spec line 67