OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedCommonOrder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One Sobolev order for the spectral and expanding-torus energy estimates

  1. theorem OAI.DefocusingNLS.radialMatched_exists_common_order line 17