OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedPenaltyFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual matched profiles instantiate every coefficient hypothesis of the singular pressure-inverse limit; no operator convergence is assumed here.

  1. theorem OAI.DefocusingNLS.radialMatched_penaltyFamily line 16