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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Rational program parameters are obtained from a single approximation to viscosity. The complete address graph, rather than its execution, is used to compute the source location and the schedule.

  1. def OAI.ForcedComputation.ExpandingDetector.programSigma line 15
  2. theorem OAI.ForcedComputation.ExpandingDetector.programSigma_pos line 17
  3. theorem OAI.ForcedComputation.ExpandingDetector.programSigma_budget line 21
  4. def OAI.ForcedComputation.ExpandingDetector.programGrowth line 33
  5. def OAI.ForcedComputation.ExpandingDetector.programFactor line 37
  6. theorem OAI.ForcedComputation.ExpandingDetector.programGrowth_val line 41
  7. theorem OAI.ForcedComputation.ExpandingDetector.programFactor_val line 46
  8. theorem OAI.ForcedComputation.ExpandingDetector.programGrowth_ge_one line 51
  9. theorem OAI.ForcedComputation.ExpandingDetector.programFactor_nonneg line 57
  10. def OAI.ForcedComputation.ExpandingDetector.initialCenterCode line 63
  11. theorem OAI.ForcedComputation.ExpandingDetector.initialCenterCode_val line 72