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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The scheduled centers have finite rational expression codes. Their formal time derivatives are the actual gate velocities.

  1. def OAI.ForcedComputation.ExpandingDetector.rampCode line 13
  2. theorem OAI.ForcedComputation.ExpandingDetector.rampCode_val line 16
  3. def OAI.ForcedComputation.ExpandingDetector.firstWeightCode line 21
  4. def OAI.ForcedComputation.ExpandingDetector.secondWeightCode line 22
  5. def OAI.ForcedComputation.ExpandingDetector.thirdWeightCode line 23
  6. theorem OAI.ForcedComputation.ExpandingDetector.weightCodes_val line 25
  7. def OAI.ForcedComputation.ExpandingDetector.centerCode line 32
  8. theorem OAI.ForcedComputation.ExpandingDetector.centerCode_val line 41
  9. theorem OAI.ForcedComputation.ExpandingDetector.centerCode_derivative line 53