SpectralRemoteMatchedRobin.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual matched weighted-Sobolev eigenpairs satisfy the uniform remote Liouville Robin estimate. Every outgoing and coefficient-symbol input is derived from the profile and eigenpair equations.

theorem OAI.DefocusingNLS.spectralRemote_matched_robin line 16