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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Whole-plane velocity detection from a terminating finite program. The program uses a single viscosity approximation to choose its schedule; each query uses a finite prefix of the full guarded instruction graph.

  1. def OAI.ForcedComputation.ExpandingDetector.compiledExpandingForce line 17
  2. def OAI.ForcedComputation.ExpandingDetector.evaluateCompiledExpandingForce line 27
  3. def OAI.ForcedComputation.ExpandingDetector.compiledExpandingForceBound line 36
  4. theorem OAI.ForcedComputation.ExpandingDetector.compiledExpandingForceBound_spec line 44
  5. theorem OAI.ForcedComputation.ExpandingDetector.compiledExpandingForce_effective line 54
  6. theorem OAI.ForcedComputation.ExpandingDetector.whole_plane_velocity_detection line 64