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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The energy uniqueness argument only needs a derivative bound on each finite interval. This covers the increasing-speed torus detector.

  1. theorem OAI.ForcedComputation.VelocityDetector.finite_interval_classical_velocity_unique line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.compact_scalar_bound line 76
  3. theorem OAI.ForcedComputation.VelocityDetector.classical_compact_derivative_bound line 86
  4. theorem OAI.ForcedComputation.VelocityDetector.classical_spatial_derivative_periodic line 96
  5. theorem OAI.ForcedComputation.VelocityDetector.classical_finite_derivative_bound line 103
  6. theorem OAI.ForcedComputation.VelocityDetector.finite_time_classical_unique line 114