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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Finite clocked expressions are closed under the full Navier–Stokes residual, including the quadratic convection term.

  1. def OAI.ForcedComputation.ClockedExpr.sum line 15
  2. theorem OAI.ForcedComputation.ClockedExpr.sum_valid line 17
  3. theorem OAI.ForcedComputation.ClockedExpr.sum_val line 23
  4. theorem OAI.ForcedComputation.ClockedExpr.sum_ofFn_valid line 31
  5. theorem OAI.ForcedComputation.ClockedExpr.sum_ofFn_val line 35
  6. def OAI.ForcedComputation.ClockedResidual.convection line 44
  7. def OAI.ForcedComputation.ClockedResidual.linear line 47
  8. def OAI.ForcedComputation.ClockedResidual.code line 51
  9. theorem OAI.ForcedComputation.ClockedResidual.convection_valid line 54
  10. theorem OAI.ForcedComputation.ClockedResidual.linear_valid line 58
  11. theorem OAI.ForcedComputation.ClockedResidual.valid line 64
  12. theorem OAI.ForcedComputation.ClockedResidual.convection_val line 67
  13. theorem OAI.ForcedComputation.ClockedResidual.linear_val line 78
  14. theorem OAI.ForcedComputation.ClockedResidual.val line 88