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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic estimate applies to an initialized field as soon as all its original derivatives are bounded. Periodicity in time is unnecessary.

  1. theorem OAI.ForcedComputation.boundedMixed_derivative line 15
  2. theorem OAI.ForcedComputation.boundedMixed_sub line 20
  3. theorem OAI.ForcedComputation.boundedMixed_sum line 30
  4. theorem OAI.ForcedComputation.bounded_uniformTimeBounds line 41
  5. theorem OAI.ForcedComputation.bounded_spatialPhase line 47
  6. theorem OAI.ForcedComputation.bounded_quadraticPhase line 53
  7. theorem OAI.ForcedComputation.bounded_viscousPhase line 63
  8. theorem OAI.ForcedComputation.bounded_profile_mixed_decay line 74
  9. theorem OAI.ForcedComputation.bounded_slowForce_spatial_time_decay line 91