OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralDilationPairing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The skew cancellation for the dilation test uses its real constant shift. This is the pointwise algebra behind the complex virial identity.

  1. def OAI.DefocusingNLS.spectralDilationCross line 10
  2. theorem OAI.DefocusingNLS.spectralDilationCross_skew line 13