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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Coordinate changes in finite field expressions. This moves the planar processor's periodic phase from its third spatial coordinate to time.

  1. def OAI.ForcedComputation.reindexPoint line 11
  2. theorem OAI.ForcedComputation.timeSpaceCoord_reindex line 14
  3. def OAI.ForcedComputation._root_.OAI.ShearFlows.FieldExpr.reindex line 18
  4. theorem OAI.ForcedComputation._root_.OAI.ShearFlows.FieldExpr.valid_reindex line 24
  5. theorem OAI.ForcedComputation._root_.OAI.ShearFlows.FieldExpr.val_reindex line 32
  6. def OAI.ForcedComputation.timeHeightSwap line 40
  7. theorem OAI.ForcedComputation.reindexPoint_timeHeightSwap line 42
  8. theorem OAI.ForcedComputation._root_.OAI.ShearFlows.FieldExpr.val_timeHeightSwap line 49