OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialLimitUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness and subsequence criteria for the C1 core limit.

  1. theorem OAI.DefocusingNLS.radial_derivative_limit_unique line 11
  2. theorem OAI.DefocusingNLS.radial_uniform_limit_of_subsequences line 26