OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHarmonicEnergy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Completed fixed-harmonic energy, including its exact angular-gradient contribution.

  1. abbrev OAI.DefocusingNLS.SpectralAngularL2 line 12
  2. def OAI.DefocusingNLS.spectralSmoothAngularValue line 14
  3. abbrev OAI.DefocusingNLS.SpectralHarmonicJet line 18
  4. def OAI.DefocusingNLS.spectralSmoothHarmonicJet line 21
  5. def OAI.DefocusingNLS.spectralHarmonicSubspace line 27
  6. abbrev OAI.DefocusingNLS.SpectralHarmonicEnergy line 30
  7. instance OAI.DefocusingNLS.spectralHarmonicEnergy_complete line 32
  8. instance OAI.DefocusingNLS.spectralHarmonicEnergy_realInner line 36
  9. def OAI.DefocusingNLS.spectralHarmonicSmoothEmbedding line 39
  10. theorem OAI.DefocusingNLS.harmonicJet_radial_mem line 44
  11. def OAI.DefocusingNLS.spectralHarmonicRadialForget line 57
  12. def OAI.DefocusingNLS.spectralHarmonicAngularValue line 63
  13. theorem OAI.DefocusingNLS.spectralHarmonicEnergy_norm_sq line 68
  14. theorem OAI.DefocusingNLS.spectralHarmonicRadialForget_smooth line 74
  15. theorem OAI.DefocusingNLS.spectralHarmonicAngularValue_smooth line 79
  16. theorem OAI.DefocusingNLS.spectralHarmonicVolume_compact line 83