OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralLiouvilleValueDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The second Liouville coordinate is the actual derivative of the first.

  1. theorem OAI.DefocusingNLS.spectralLiouville_value_hasDerivAt line 9
  2. theorem OAI.DefocusingNLS.spectralPhysicalLiouvillePair_value_hasDerivAt line 19