OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralClosedExtensionRegularity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the endpoint derivatives supplied by the weak-flux extension.

  1. theorem OAI.DefocusingNLS.spectralSecondDerivativeValue_continuousOn_closed line 10
  2. theorem OAI.DefocusingNLS.spectralSecond_closedExtension_C1 line 23