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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Local effective bounds for clocked expressions. Periodic field factors have global bounds; only the explicit clock profiles use a time radius.

  1. def OAI.ForcedComputation.ClockedExpr.bound line 13
  2. theorem OAI.ForcedComputation.ClockedExpr.bound_nonneg line 20
  3. theorem OAI.ForcedComputation.ClockedExpr.val_bound line 28
  4. def OAI.ForcedComputation.ClockedExpr.diffWord line 42
  5. theorem OAI.ForcedComputation.ClockedExpr.valid_diffWord line 46
  6. def OAI.ForcedComputation.ClockedExpr.scalarMixed line 52
  7. theorem OAI.ForcedComputation.ClockedExpr.val_diffWord line 55
  8. theorem OAI.ForcedComputation.ClockedExpr.mixed_bound line 65