OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/DetectorForceProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The evaluator selects a finite clocked program from the zeroth time approximation. Locality of the residual certifies every mixed derivative.

  1. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_congr_germ line 15
  2. theorem OAI.ForcedComputation.VelocityDetector.detectorForce_prefix_germ line 29
  3. def OAI.ForcedComputation.VelocityDetector.forcePrefixLength line 48
  4. theorem OAI.ForcedComputation.VelocityDetector.forcePrefixLength_bound line 50
  5. def OAI.ForcedComputation.VelocityDetector.evaluateDetectorForce line 56
  6. theorem OAI.ForcedComputation.VelocityDetector.evaluateDetectorForce_spec line 62
  7. def OAI.ForcedComputation.VelocityDetector.detectorForceBound line 78
  8. theorem OAI.ForcedComputation.VelocityDetector.detectorForceBound_nonneg line 81
  9. theorem OAI.ForcedComputation.VelocityDetector.detectorForceBound_spec line 85