OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningForbiddenGreen.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Constructed Green data for the actual outgoing family on its forbidden outer interval. There are no assumed comparison solutions or Wronskians.

  1. theorem OAI.DefocusingNLS.spectralTurning_outgoing_forbidden_green line 12