OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralGrowingBranchCone.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A controlled residual and an exponentially smaller second branch leave the actual Cauchy data in the growing branch's Robin cone.

  1. theorem OAI.DefocusingNLS.spectralGrowingBranch_error line 10
  2. theorem OAI.DefocusingNLS.spectralGrowingBranch_cone line 37
  3. theorem OAI.DefocusingNLS.spectralGrowingBranch_relative_cone line 60
  4. theorem OAI.DefocusingNLS.spectralGrowingBranch_value_lower line 89