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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite smooth expressions for the moving whole-plane gates. Unlike periodic field expressions, their profile arguments may depend on both time and position. The only nonpolynomial primitives are the existing effective flat glue and its everywhere positive transition denominator.

  1. inductive OAI.ForcedComputation.SmoothAtom line 14
  2. def OAI.ForcedComputation.SmoothAtom.profile line 19
  3. inductive OAI.ForcedComputation.NonperiodicExpr line 23
  4. def OAI.ForcedComputation.NonperiodicExpr.val line 33
  5. def OAI.ForcedComputation.NonperiodicExpr.sub line 40
  6. def OAI.ForcedComputation.NonperiodicExpr.composeProfile line 42
  7. theorem OAI.ForcedComputation.NonperiodicExpr.val_composeProfile line 50
  8. def OAI.ForcedComputation.NonperiodicExpr.diff line 60
  9. theorem OAI.ForcedComputation.NonperiodicExpr.smooth line 67
  10. theorem OAI.ForcedComputation.NonperiodicExpr.val_diff line 75
  11. def OAI.ForcedComputation.NonperiodicExpr.diffWord line 106
  12. theorem OAI.ForcedComputation.NonperiodicExpr.val_diffWord line 110