OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/CompactPlanarBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Bounds and actual global transitions for the compact planar version of the normalized program. The periodic spatial expression agrees on the chart; outside the common support all derivatives vanish.

  1. def OAI.ForcedComputation.Recorder.Planar.compactVelocity line 15
  2. theorem OAI.ForcedComputation.Recorder.Planar.compactVelocity_smooth line 21
  3. theorem OAI.ForcedComputation.Recorder.Planar.compactVelocity_germ line 26
  4. theorem OAI.ForcedComputation.Recorder.Planar.compactVelocity_support line 36
  5. theorem OAI.ForcedComputation.Recorder.Planar.compactVelocity_off_chart line 41
  6. theorem OAI.ForcedComputation.Recorder.Planar.compactVelocity_bound line 50
  7. theorem OAI.ForcedComputation.Recorder.Planar.compactVelocity_derivative_bounds line 61
  8. theorem OAI.ForcedComputation.Recorder.Planar.compactVelocity_lipschitz line 82
  9. theorem OAI.ForcedComputation.Recorder.Planar.compactVelocity_transitions line 93