OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialFirstMassLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The first gauge component has vanishing weighted L2 mass along every escaping frequency sequence with bounded energy and boundary pairing.

  1. theorem OAI.DefocusingNLS.spectralFrequency_mass_limit line 13
  2. theorem OAI.DefocusingNLS.radialMatched_first_mass_limit line 33