OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHarmonicForm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The weighted base form, including the harmonic angular derivative.

  1. structure OAI.DefocusingNLS.SpectralHarmonicWeight line 12
  2. def OAI.DefocusingNLS.spectralHarmonicValue line 20
  3. def OAI.DefocusingNLS.spectralHarmonicDerivative line 24
  4. def OAI.DefocusingNLS.spectralHarmonicForm line 28
  5. theorem OAI.DefocusingNLS.spectralHarmonicForm_lower line 40
  6. def OAI.DefocusingNLS.spectralHarmonicPairForm line 62
  7. theorem OAI.DefocusingNLS.spectralHarmonicPairForm_lower line 71
  8. theorem OAI.DefocusingNLS.spectralHarmonicPairForm_coercive line 81