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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of the prescribed whole-plane force from finite names. Only a finite initial segment of the complete guarded graph is inspected.

  1. theorem OAI.ForcedComputation.ExpandingDetector.prefixCode_germ line 17
  2. def OAI.ForcedComputation.ExpandingDetector.expandingPrefixLength line 34
  3. theorem OAI.ForcedComputation.ExpandingDetector.expandingPrefixLength_bound line 36
  4. def OAI.ForcedComputation.ExpandingDetector.evaluateExpandingForce line 42
  5. theorem OAI.ForcedComputation.ExpandingDetector.evaluateExpandingForce_spec line 50