OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHarmonicWeightDifference.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform mass-weight convergence controls the complete harmonic base form.

  1. theorem OAI.DefocusingNLS.spectralHarmonicCoordinate_norms line 11
  2. theorem OAI.DefocusingNLS.spectralHarmonicForm_difference_bound line 28