OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralSubunitDifference.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A quantitative Lipschitz constant for the spectral coefficient pair. It tends to zero on a fixed subunit disk, even after division by the exponential order of the profile remainder.

  1. theorem OAI.DefocusingNLS.spectral_power_difference_bound line 12
  2. theorem OAI.DefocusingNLS.spectral_mixed_power_difference_bound line 30
  3. theorem OAI.DefocusingNLS.spectralCoefficient_subunit_difference line 48
  4. theorem OAI.DefocusingNLS.spectralCoefficient_difference_rate_tendsto line 84
  5. theorem OAI.DefocusingNLS.spectralCoefficient_weighted_difference line 95
  6. theorem OAI.DefocusingNLS.radialShooting_spectralDifference_uniform_small line 117