OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralDilationDecomposition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the derivative in this decomposition separates the real volume pairing from the imaginary boundary flux.

  1. theorem OAI.DefocusingNLS.spectralDilationCross_decomposition line 10