OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialPotentialDifference.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Quantitative dependence of the actual inner potential on its amplitude.

  1. theorem OAI.DefocusingNLS.radialAverage_sub line 12
  2. theorem OAI.DefocusingNLS.radial_unit_square_difference line 22
  3. theorem OAI.DefocusingNLS.radialAverage_square_difference line 31
  4. theorem OAI.DefocusingNLS.radial_velocity_quotient_difference line 53
  5. theorem OAI.DefocusingNLS.radialAverage_unit_square_bounds line 88
  6. theorem OAI.DefocusingNLS.radialVelocityRatio_difference line 102
  7. theorem OAI.DefocusingNLS.radialAmplitudePotential_difference line 114
  8. theorem OAI.DefocusingNLS.radialAmplitudePotential_congr line 142