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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The injection and stirring clocks are finite rational profile expressions. Their symbolic derivatives give the prescribed rates.

  1. def OAI.ForcedComputation.VelocityDetector.blockStart line 12
  2. def OAI.ForcedComputation.VelocityDetector.injectionExpression line 14
  3. def OAI.ForcedComputation.VelocityDetector.phaseExpression line 17
  4. theorem OAI.ForcedComputation.VelocityDetector.smoothRamp_window line 22
  5. theorem OAI.ForcedComputation.VelocityDetector.injectionExpression_val line 28
  6. theorem OAI.ForcedComputation.VelocityDetector.phaseExpression_val line 37
  7. theorem OAI.ForcedComputation.VelocityDetector.injectionExpression_diff_val line 51
  8. theorem OAI.ForcedComputation.VelocityDetector.phaseExpression_diff_val line 57