OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralParameterGrowth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Polynomial differentiation for the ten coordinates of the profile, outgoing column and its parameter derivative. The fixed dimension is exactly what the generalized-mode outgoing estimate needs.

  1. inductive OAI.DefocusingNLS.SpectralParameterExpr line 17
  2. def OAI.DefocusingNLS.SpectralParameterExpr.eval line 27
  3. def OAI.DefocusingNLS.SpectralParameterExpr.pow line 35
  4. theorem OAI.DefocusingNLS.SpectralParameterExpr.eval_pow line 39
  5. def OAI.DefocusingNLS.SpectralParameterExpr.differentiate line 45
  6. theorem OAI.DefocusingNLS.SpectralParameterExpr.hasDerivAt_eval line 54
  7. theorem OAI.DefocusingNLS.SpectralParameterExpr.iteratedDeriv_eval line 70
  8. theorem OAI.DefocusingNLS.SpectralParameterExpr.eval_exponential_bound line 87
  9. theorem OAI.DefocusingNLS.SpectralParameterExpr.derivatives_exponential_bound line 140