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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Periodic profiles supply the logarithmic-force bounds

The phase bounds used in the slow-clock estimate follow from smoothness and periodicity of the original field. They are not extra decay assumptions.

  1. theorem OAI.ForcedComputation.iteratedDeriv_eq_mixedTime line 19
  2. theorem OAI.ForcedComputation.periodic_uniformTimeBounds line 34
  3. theorem OAI.ForcedComputation.quadraticPhase_smooth line 41
  4. theorem OAI.ForcedComputation.quadraticPhase_spatially_periodic line 45
  5. theorem OAI.ForcedComputation.quadraticPhase_time_periodic line 62
  6. theorem OAI.ForcedComputation.viscousPhase_smooth line 72
  7. theorem OAI.ForcedComputation.viscousPhase_spatially_periodic line 75
  8. theorem OAI.ForcedComputation.viscousPhase_time_periodic line 86
  9. theorem OAI.ForcedComputation.quadraticPhase_uniformTimeBounds line 95
  10. theorem OAI.ForcedComputation.viscousPhase_uniformTimeBounds line 102
  11. theorem OAI.ForcedComputation.periodic_slowForce_time_decay line 109