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

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The repeated compact Euclidean field depends only on the machine. Its fixed vertical cutoff leaves the planar computation on height zero exact.

  1. def OAI.ForcedComputation.BalancedBody.verticalCutoff line 15
  2. theorem OAI.ForcedComputation.BalancedBody.verticalCutoff_smooth line 17
  3. theorem OAI.ForcedComputation.BalancedBody.verticalCutoff_zero line 20
  4. def OAI.ForcedComputation.BalancedBody.raw line 23
  5. def OAI.ForcedComputation.BalancedBody.velocity line 26
  6. def OAI.ForcedComputation.BalancedBody.rawSupport line 29
  7. def OAI.ForcedComputation.BalancedBody.support line 31
  8. theorem OAI.ForcedComputation.BalancedBody.rawSupport_compact line 33
  9. theorem OAI.ForcedComputation.BalancedBody.support_compact line 35
  10. theorem OAI.ForcedComputation.BalancedBody.raw_smooth line 38
  11. theorem OAI.ForcedComputation.BalancedBody.velocity_smooth line 43
  12. theorem OAI.ForcedComputation.BalancedBody.raw_support line 46
  13. theorem OAI.ForcedComputation.BalancedBody.velocity_support line 73
  14. theorem OAI.ForcedComputation.BalancedBody.raw_divergence line 80
  15. theorem OAI.ForcedComputation.BalancedBody.velocity_divergence line 94
  16. theorem OAI.ForcedComputation.BalancedBody.raw_periodic line 98
  17. theorem OAI.ForcedComputation.BalancedBody.velocity_periodic line 105
  18. theorem OAI.ForcedComputation.BalancedBody.velocity_bounded line 112