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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A computable modulus on each finite time slab for the detector's clocked expressions. Spatial coordinates remain unrestricted.

  1. def OAI.ForcedComputation.ClockedExpr.derivativeBound line 12
  2. theorem OAI.ForcedComputation.ClockedExpr.derivativeBound_nonneg line 15
  3. theorem OAI.ForcedComputation.ClockedExpr.fderiv_bound line 18
  4. theorem OAI.ForcedComputation.ClockedExpr.lipschitz_bound line 41