OAI/MathematicalPhysics/DefocusingNLS/Certificates/HighAngularArc.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Geometry and positivity on the initial arc of the high-angular contour.

  1. def OAI.DefocusingNLS.highArcAngle line 10
  2. def OAI.DefocusingNLS.highArcU line 11
  3. def OAI.DefocusingNLS.highArcV line 12
  4. def OAI.DefocusingNLS.highArcL line 13
  5. def OAI.DefocusingNLS.highArcN line 16
  6. theorem OAI.DefocusingNLS.highArc_sin_cos line 20
  7. theorem OAI.DefocusingNLS.highArc_geometry line 36
  8. def OAI.DefocusingNLS.highArcPotential line 66
  9. theorem OAI.DefocusingNLS.highArcPotential_pos line 71
  10. theorem OAI.DefocusingNLS.highArc_join_L line 81
  11. theorem OAI.DefocusingNLS.highArc_join_jump_pos line 87