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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The periodically repeated loading row is used once. Every later material step belongs to the fresh recorder, whose orbit never returns to that row.

  1. def OAI.ForcedComputation.Recorder.periodicStartingPoint line 13
  2. theorem OAI.ForcedComputation.Recorder.periodicLoader_center line 15
  3. theorem OAI.ForcedComputation.Recorder.periodicLoader_contains line 23
  4. theorem OAI.ForcedComputation.Recorder.periodicLoading_endpoint line 34
  5. theorem OAI.ForcedComputation.Recorder.Steps.flow_loaded line 54
  6. theorem OAI.ForcedComputation.Recorder.periodicLoading_safe line 71