OAI/MathematicalPhysics/DefocusingNLS/Certificates/ShiftedSlowGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Weighted integrability of the shifted slow solution

Every spatial derivative has polynomial growth along the translated positive ray. Exponential weighting therefore makes its product with any polynomial integrable, as required in the Laguerre projection.

  1. def OAI.DefocusingNLS.shiftedSlowDerivative line 19
  2. theorem OAI.DefocusingNLS.shiftedSlowDerivative_zero line 22
  3. theorem OAI.DefocusingNLS.hasDerivAt_shiftedSlowDerivative line 25
  4. theorem OAI.DefocusingNLS.continuous_shiftedSlowDerivative line 37
  5. theorem OAI.DefocusingNLS.shiftedSlowDerivative_isBigO_rpow line 42
  6. theorem OAI.DefocusingNLS.polynomial_eval_isBigO_exp line 66
  7. theorem OAI.DefocusingNLS.integrableOn_exp_neg_mul_polynomial_of_growth line 77
  8. theorem OAI.DefocusingNLS.integrableOn_laguerreIntegrand_shiftedSlowDerivative line 101