OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralShellInnerRobin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The coupled Green error gives both local Robin errors, including when one of the channel values is zero.

  1. theorem OAI.DefocusingNLS.spectralCoupled_inner_robin_bound line 11
  2. theorem OAI.DefocusingNLS.spectralCoupled_inner_robin_scaled line 27