OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSpectralGrowth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Coarse derivative growth for the coupled profile and spectral state

The six scalar coordinates form a polynomial differential system with the single explicit coefficient exp(2t). This records coarse derivative growth, independent of the order of any comparison polynomial.

  1. inductive OAI.DefocusingNLS.HomogeneousSpectralExpr line 20
  2. def OAI.DefocusingNLS.HomogeneousSpectralExpr.eval line 30
  3. def OAI.DefocusingNLS.HomogeneousSpectralExpr.pow line 38
  4. theorem OAI.DefocusingNLS.HomogeneousSpectralExpr.eval_pow line 42
  5. def OAI.DefocusingNLS.HomogeneousSpectralExpr.differentiate line 48
  6. theorem OAI.DefocusingNLS.HomogeneousSpectralExpr.hasDerivAt_eval line 57
  7. theorem OAI.DefocusingNLS.HomogeneousSpectralExpr.iteratedDeriv_eval line 73
  8. theorem OAI.DefocusingNLS.HomogeneousSpectralExpr.eval_exponential_bound line 90
  9. theorem OAI.DefocusingNLS.HomogeneousSpectralExpr.derivatives_exponential_bound line 143