OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingDerivativeWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One physical derivative costs one high-frequency Sobolev order uniformly in radius

  1. theorem OAI.DefocusingNLS.derivative_density_bound line 9
  2. theorem OAI.DefocusingNLS.expandingSobolevWeight_derivative_le line 65