OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHarmonicObservation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The fixed-harmonic pair space, compact observation, and closed core constraint.

  1. abbrev OAI.DefocusingNLS.SpectralHarmonicPair line 10
  2. instance OAI.DefocusingNLS.spectralHarmonicPair_realInner line 13
  3. def OAI.DefocusingNLS.spectralHarmonicPairForget line 16
  4. def OAI.DefocusingNLS.spectralHarmonicObservation line 25
  5. theorem OAI.DefocusingNLS.spectralHarmonicObservation_compact line 29
  6. def OAI.DefocusingNLS.spectralHarmonicFirstValue line 33
  7. def OAI.DefocusingNLS.spectralHarmonicCoreSubspace line 37
  8. abbrev OAI.DefocusingNLS.SpectralHarmonicCore line 41
  9. instance OAI.DefocusingNLS.spectralHarmonicCore_normedSpace line 44
  10. instance OAI.DefocusingNLS.spectralHarmonicCore_inner line 47
  11. instance OAI.DefocusingNLS.spectralHarmonicCore_complete line 50
  12. theorem OAI.DefocusingNLS.spectralHarmonicCore_mem line 56