OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedPressureTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual inner pressure transport has the required small relative upper bound.

  1. theorem OAI.DefocusingNLS.radialMatchedInnerPressure_transport line 12