OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralClassicalPairing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Classical representatives and their exact completed-space test pairings.

  1. theorem OAI.DefocusingNLS.spectralHarmonicValue_classical_ae line 13
  2. theorem OAI.DefocusingNLS.spectralHarmonicScalar_classical_pairing line 21
  3. theorem OAI.DefocusingNLS.spectralPressure_classical_pairing line 51
  4. theorem OAI.DefocusingNLS.spectralHarmonicClassical_zero_of_value line 73
  5. theorem OAI.DefocusingNLS.spectralObservation_ne_zero_of_classical line 84
  6. theorem OAI.DefocusingNLS.realPart_inner line 99
  7. def OAI.DefocusingNLS.SpectralPenaltyFamily.penaltyComplexForm line 108
  8. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.penaltyComplexForm_re line 116
  9. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.compactPencil_of_complex_tests line 123