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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The periodic-initialization main theorem of Geometric Programs for Solenoidal Forcing. The finite program repeats its loading instruction, but the fresh recorder never returns to that instruction's source or target.

  1. def OAI.ForcedComputation.PeriodicFluidProperties line 14
  2. theorem OAI.ForcedComputation.periodic_bundle line 27
  3. def OAI.ForcedComputation.periodicProgram line 42
  4. def OAI.ForcedComputation.periodicVelocity line 45
  5. def OAI.ForcedComputation.periodicForce line 48
  6. theorem OAI.ForcedComputation.periodic_effective_computation line 51