OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPolynomialUniformLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform polynomial estimates needed for the normalized outgoing residual. High polynomial degrees of the nonlinear coefficients are allowed.

  1. theorem OAI.DefocusingNLS.spectralPolynomial_subunit_uniform_limit line 12
  2. theorem OAI.DefocusingNLS.spectralPolynomial_mul_uniform_zero line 42
  3. theorem OAI.DefocusingNLS.spectralPolynomial_star_uniform_zero line 74