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

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

A finite rational program for the complete balanced velocity on any bounded time window. The repeated portion is compiled from the machine alone; the input affects only the translation used during loading.

  1. def OAI.ForcedComputation.BalancedExpressions.substitute line 15
  2. theorem OAI.ForcedComputation.BalancedExpressions.substitute_val line 22
  3. def OAI.ForcedComputation.BalancedExpressions.inverseCoordinates line 32
  4. theorem OAI.ForcedComputation.BalancedExpressions.inverseCoordinates_val line 35
  5. def OAI.ForcedComputation.BalancedExpressions.stretchCode line 47
  6. theorem OAI.ForcedComputation.BalancedExpressions.stretchCode_val line 50
  7. def OAI.ForcedComputation.BalancedExpressions.verticalCode line 59
  8. theorem OAI.ForcedComputation.BalancedExpressions.verticalCode_val line 62
  9. def OAI.ForcedComputation.BalancedExpressions.liftCode line 69
  10. theorem OAI.ForcedComputation.BalancedExpressions.liftCode_val line 71
  11. def OAI.ForcedComputation.BalancedExpressions.bodyCode line 76
  12. theorem OAI.ForcedComputation.BalancedExpressions.bodyCode_val line 80
  13. def OAI.ForcedComputation.BalancedExpressions.loaderPrimitive line 96
  14. def OAI.ForcedComputation.BalancedExpressions.loaderPotentialCode line 98
  15. theorem OAI.ForcedComputation.BalancedExpressions.loaderPotentialCode_val line 101
  16. def OAI.ForcedComputation.BalancedExpressions.loaderCode line 112
  17. theorem OAI.ForcedComputation.BalancedExpressions.loaderCode_val line 116
  18. def OAI.ForcedComputation.BalancedExpressions.activationCode line 145
  19. theorem OAI.ForcedComputation.BalancedExpressions.activationCode_val line 150
  20. def OAI.ForcedComputation.BalancedExpressions.code line 155
  21. theorem OAI.ForcedComputation.BalancedExpressions.code_val line 159
  22. theorem OAI.ForcedComputation.BalancedExpressions.code_germ line 170