OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousGluedLocalL2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Origin regularity and a strict power bound give the required radial top energy.

  1. theorem OAI.DefocusingNLS.homogeneousGlued_local_top_integrable line 12
  2. theorem OAI.DefocusingNLS.homogeneousGlued_top_integrable line 28