OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHarmonicPhase.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of the complete harmonic form with multiplication by i.

  1. theorem OAI.DefocusingNLS.spectralHarmonicForm_I line 11
  2. theorem OAI.DefocusingNLS.spectralHarmonicPairForm_I line 29