OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialODEGrowthExpression.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A concrete differential algebra for the exterior radial ODE

Every time derivative of the bounded exterior state is a finite expression in its two components, their conjugates, and exp(2t). This syntax records that elementary fact without expanding large higher derivatives.

  1. inductive OAI.DefocusingNLS.RadialODEExpr line 18
  2. def OAI.DefocusingNLS.RadialODEExpr.eval line 29
  3. def OAI.DefocusingNLS.RadialODEExpr.pow line 38
  4. theorem OAI.DefocusingNLS.RadialODEExpr.eval_pow line 42
  5. def OAI.DefocusingNLS.RadialODEExpr.acceleration line 48
  6. theorem OAI.DefocusingNLS.RadialODEExpr.eval_acceleration line 54
  7. def OAI.DefocusingNLS.RadialODEExpr.differentiate line 62
  8. theorem OAI.DefocusingNLS.RadialODEExpr.hasDerivAt_eval line 71
  9. theorem OAI.DefocusingNLS.RadialODEExpr.iteratedDeriv_position line 87