OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedWeakPhysical.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual weak limiting equation gives a classical physical solution with its outer Robin trace.

  1. theorem OAI.DefocusingNLS.radialMatchedWeak_physical_extension_of_boundary line 13
  2. theorem OAI.DefocusingNLS.radialMatchedWeak_physical_extension line 65