OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralScalarGreenRepresentation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Mixed endpoint variation of constants. Every actual scalar solution is recovered from its left outgoing coefficient, right Dirichlet coefficient, and the Green integral, without a separate uniqueness assumption.

  1. theorem OAI.DefocusingNLS.spectralScalarWronskian_forced line 12
  2. theorem OAI.DefocusingNLS.spectralScalarWronskian_decomposition line 27
  3. theorem OAI.DefocusingNLS.spectralScalarGreen_representation line 40