OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHarmonicScalarPairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The scalar test identity of the weighted harmonic form, including its angular term.

  1. theorem OAI.DefocusingNLS.spectral_star_inner line 12
  2. theorem OAI.DefocusingNLS.spectralHarmonicAngular_smooth_ae line 16
  3. theorem OAI.DefocusingNLS.spectralHarmonicScalar_pairing line 30