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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic slowdown is extended smoothly through all negative times. The given zero collar removes the apparent singularity of the logarithm.

  1. def OAI.ForcedComputation.slowFromRest line 17
  2. theorem OAI.ForcedComputation.slowFromRest_before line 20
  3. theorem OAI.ForcedComputation.slowFromRest_eq line 23
  4. theorem OAI.ForcedComputation.slowFromRest_zero_collar line 31
  5. theorem OAI.ForcedComputation.slowFromRest_smooth line 42
  6. theorem OAI.ForcedComputation.slowFromRest_periodic line 62
  7. theorem OAI.ForcedComputation.slowFromRest_solenoidal line 70
  8. theorem OAI.ForcedComputation.slowFromRest_zero_advection line 79
  9. theorem OAI.ForcedComputation.slowFromRest_mean_zero line 88
  10. theorem OAI.ForcedComputation.slowFromRest_solution line 97
  11. theorem OAI.ForcedComputation.slowFromRest_uniform_bound line 106
  12. theorem OAI.ForcedComputation.slowFromRest_lipschitz line 116
  13. theorem OAI.ForcedComputation.slowFromRest_materialFlow line 136
  14. theorem OAI.ForcedComputation.slowFromRest_trace line 148
  15. theorem OAI.ForcedComputation.slowFromRest_reaches_iff line 167