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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean estimates also hold for the compact extension. In the chart its transition is locally the periodic transition, and outside the common support its transition is locally the identity.

  1. theorem OAI.ForcedComputation.euclideanMap_eventuallyEq line 16
  2. theorem OAI.ForcedComputation.Recorder.Planar.compact_euclidean_field_bounds line 24
  3. theorem OAI.ForcedComputation.Recorder.Planar.compactTransition_euclidean_germ line 57
  4. theorem OAI.ForcedComputation.Recorder.Planar.compactTransition_euclidean_smooth line 74
  5. theorem OAI.ForcedComputation.Recorder.Planar.compactTransition_euclidean_transfer line 87
  6. theorem OAI.ForcedComputation.Recorder.Planar.compact_euclidean_flow_estimates line 108