OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralOutgoingPolynomialLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite normalized outgoing expansions converge to the decoupled free expansions. No convergence of regular columns through the core is used.

  1. theorem OAI.DefocusingNLS.spectralPolynomial_mul_zero_coefficient_limit line 12
  2. theorem OAI.DefocusingNLS.spectralPolynomialResidual_zero_coefficient_limit line 20
  3. theorem OAI.DefocusingNLS.spectralStarPolynomial_zero_coefficient_limit line 40
  4. theorem OAI.DefocusingNLS.spectralOutgoingPolynomial_coefficient_limit line 47