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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The observation argument for the autonomous suspension. The finite processor supplies one-period branch trajectories, whose all-time consequence is proved for the actual material flow.

  1. def OAI.ForcedComputation.stationaryObserver line 14
  2. def OAI.ForcedComputation.stationaryStartingPoint line 20
  3. theorem OAI.ForcedComputation.Recorder.Planar.shifted_suspension_observation line 26
  4. theorem OAI.ForcedComputation.Recorder.Planar.normalized_suspension_observation line 102