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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every spatial derivative of the slow force has the same integrable time decay. The phase fields are the actual acceleration and Laplacian of the original periodic velocity.

  1. theorem OAI.ForcedComputation.spatialWord_smooth line 15
  2. theorem OAI.ForcedComputation.spatialWord_sub line 21
  3. theorem OAI.ForcedComputation.spatialWord_slowForce line 35
  4. theorem OAI.ForcedComputation.periodic_slowForce_spatial_time_decay line 58