OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteUniformRobin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform physical Robin data obtained from the remote ODE and outgoing logarithmic symbols. No endpoint condition is assumed.

  1. theorem OAI.DefocusingNLS.spectralRemote_uniform_robin line 12