OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/SlowEffective.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A terminating evaluator for every mixed derivative of the slow force. Its only inputs beyond the finite rational program are fast names for the viscosity and the evaluation point.

  1. theorem OAI.ForcedComputation.slowCoarseTimeBound line 14
  2. theorem OAI.ForcedComputation.slowCoarsePositive line 20
  3. def OAI.ForcedComputation.evaluateSlowForce line 25
  4. theorem OAI.ForcedComputation.evaluateSlowForce_spec line 36