OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralMatchedShellAbsorption.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absorption for the matched weighted-Sobolev eigenpair, using its remote Robin condition and coupled forcing bounds.

  1. theorem OAI.DefocusingNLS.spectralMatched_shell_absorption line 13