OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingLowerWeightBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lower-order frequency weight controlled by mass and top derivatives

  1. theorem OAI.DefocusingNLS.lowerFrequencyWeight_le_mass_top line 9
  2. theorem OAI.DefocusingNLS.expandingLowerWeight_le_mass_top line 30