OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCaseIIRobinCoercivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two mixed Case II Robin slopes control local values by local first derivatives when the actual Green error is sufficiently small.

  1. theorem OAI.DefocusingNLS.spectralNoTurn_ratio_norm_lower line 14
  2. theorem OAI.DefocusingNLS.spectralCaseII_robin_coercivity line 31