OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialExteriorNonlinearUniqueness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The full outgoing expansion uniquely selects a nonlinear exterior solution.

  1. theorem OAI.DefocusingNLS.radialExterior_forced_gauge_derivative line 13
  2. theorem OAI.DefocusingNLS.radialExterior_nonlinear_fast_decay_unique line 31
  3. theorem OAI.DefocusingNLS.radialExterior_same_expansion_unique line 87