OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialInnerDeformation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Direct positive deformation in the inner ball from the proved slope estimate.

  1. theorem OAI.DefocusingNLS.radialVelocity_hasDerivAt_zero line 13
  2. theorem OAI.DefocusingNLS.radialMatched_inner_deformation line 31