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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The zeroth time approximation selects a finite translate window with one unit of spare width. Evaluation of every residual jet is then the existing terminating finite-expression evaluator, including a viscosity name when viscosity is not rational.

  1. def OAI.ForcedComputation.BalancedExpressions.windowLower line 15
  2. def OAI.ForcedComputation.BalancedExpressions.windowUpper line 16
  3. theorem OAI.ForcedComputation.BalancedExpressions.named_window line 18
  4. def OAI.ForcedComputation.BalancedExpressions.evaluate line 27
  5. theorem OAI.ForcedComputation.BalancedExpressions.evaluate_spec line 32
  6. def OAI.ForcedComputation.BalancedExpressions.boxForceBound line 43
  7. theorem OAI.ForcedComputation.BalancedExpressions.boxForceBound_spec line 49