OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialCanonicalParameterL2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual outgoing parameter derivative has finite top energy in the counting half-plane.

  1. theorem OAI.DefocusingNLS.radialCanonicalParameter_top_integrable line 13
  2. theorem OAI.DefocusingNLS.radialCanonicalParameter_eventually_bounded line 39