OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralClassicalObservationLine.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Recovering proportional classical functions from compact observations
- theorem
OAI.DefocusingNLS.spectralClassical_pair_eq_of_observationline 12