OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/SuspensionExpressions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

A finite Hamiltonian expression gives an autonomous finite velocity expression after adding the fixed spatial clock.

  1. def OAI.ForcedComputation.SpatialExpression.NoTime line 15
  2. def OAI.ForcedComputation.SpatialExpression.UnitPeriods line 20
  3. theorem OAI.ForcedComputation.SpatialExpression.noTime_diff line 24
  4. def OAI.ForcedComputation.SpatialExpression.spatialValue line 34
  5. theorem OAI.ForcedComputation.SpatialExpression.unitPeriods_periodic line 36
  6. theorem OAI.ForcedComputation.SpatialExpression.noTime_val line 57
  7. theorem OAI.ForcedComputation.SpatialExpression.spatialValue_smooth line 67
  8. theorem OAI.ForcedComputation.SpatialExpression.spatialValue_diff line 71
  9. def OAI.ForcedComputation.SpatialExpression.suspensionCode line 83
  10. theorem OAI.ForcedComputation.SpatialExpression.suspensionCode_valid line 87
  11. theorem OAI.ForcedComputation.SpatialExpression.suspensionCode_noTime line 94
  12. def OAI.ForcedComputation.SpatialExpression.suspensionField line 102
  13. theorem OAI.ForcedComputation.SpatialExpression.suspensionCode_val line 107
  14. theorem OAI.ForcedComputation.SpatialExpression.suspensionField_eq line 117
  15. theorem OAI.ForcedComputation.SpatialExpression.suspensionField_smooth line 122
  16. theorem OAI.ForcedComputation.SpatialExpression.suspensionField_divergence line 127
  17. theorem OAI.ForcedComputation.SpatialExpression.suspensionField_mean_zero line 144
  18. theorem OAI.ForcedComputation.SpatialExpression.suspensionField_periodic line 160