OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialCoercivityBoundary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The upper-half-plane coercivity estimate with a controlled boundary trace.

  1. theorem OAI.DefocusingNLS.radialScalarForm_coercive_boundary line 13
  2. theorem OAI.DefocusingNLS.radialMatched_spectral_coercivity_boundary line 33