OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralScalarUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local uniqueness from two constructed comparison solutions and conserved Wronskians. No global coefficient extension is required.

  1. theorem OAI.DefocusingNLS.spectralScalar_unique_right line 12