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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The compact planar flow fixes every point off its common support and preserves that support. In particular, its trajectories cannot leave the unit-square chart.

  1. theorem OAI.ForcedComputation.Recorder.Planar.compactTransition_fixed line 13
  2. theorem OAI.ForcedComputation.Recorder.Planar.compactTransition_support line 25
  3. theorem OAI.ForcedComputation.Recorder.Planar.compactTransition_chart line 35
  4. theorem OAI.ForcedComputation.Recorder.Planar.compactTransition_eq_slice line 46