OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPhysicalOscillatoryEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual eigenpair inherits the no-turn shell energy estimate; its coefficient equation and forcing continuity are discharged internally.

  1. theorem OAI.DefocusingNLS.spectralPhysicalLiouvillePair_oscillatory_energy line 12