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

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The compact Euclidean velocity is the input loader followed by the machine-only periodic processor. Its full Navier--Stokes residual is affine in viscosity and has the same fixed compact spatial support.

  1. def OAI.ForcedComputation.BalancedVelocity.velocity line 16
  2. def OAI.ForcedComputation.BalancedVelocity.support line 19
  3. theorem OAI.ForcedComputation.BalancedVelocity.support_compact line 21
  4. theorem OAI.ForcedComputation.BalancedVelocity.smooth line 24
  5. theorem OAI.ForcedComputation.BalancedVelocity.supported line 28
  6. theorem OAI.ForcedComputation.BalancedVelocity.before line 35
  7. theorem OAI.ForcedComputation.BalancedVelocity.tail line 40
  8. theorem OAI.ForcedComputation.BalancedVelocity.zero_before line 46
  9. theorem OAI.ForcedComputation.BalancedVelocity.solenoidal line 50
  10. theorem OAI.ForcedComputation.BalancedVelocity.bounded line 73
  11. theorem OAI.ForcedComputation.BalancedVelocity.residual_zero line 82
  12. theorem OAI.ForcedComputation.BalancedVelocity.residual_supported line 95
  13. theorem OAI.ForcedComputation.BalancedVelocity.residual_periodic line 112
  14. theorem OAI.ForcedComputation.BalancedVelocity.force_supported line 122
  15. theorem OAI.ForcedComputation.BalancedVelocity.force_bounded line 126
  16. def OAI.ForcedComputation.BalancedVelocity.force₀ line 145
  17. def OAI.ForcedComputation.BalancedVelocity.force₁ line 148
  18. theorem OAI.ForcedComputation.BalancedVelocity.force_affine line 151