OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingSobolevComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The fixed expanding norm is equivalent to the usual Sobolev norm

The weight comparison at radius one identifies the expanding-space solution with the standard Sobolev flow.

  1. theorem OAI.DefocusingNLS.expandingSobolevWeightSq_one_le_standard line 13
  2. theorem OAI.DefocusingNLS.standard_le_expandingSobolevWeightSq_one line 25
  3. theorem OAI.DefocusingNLS.sqrt_standard_power line 48
  4. theorem OAI.DefocusingNLS.expandingSobolevWeight_one_le_standard line 54
  5. theorem OAI.DefocusingNLS.standard_le_expandingSobolevWeight_one line 63