OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingOrderedSymbol.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scale-uniform frequency gain for the ordered torus commutator

  1. def OAI.DefocusingNLS.expandingOrderedFactor line 11
  2. theorem OAI.DefocusingNLS.expandingOrderedFactor_nonneg line 14
  3. theorem OAI.DefocusingNLS.expandingOrderedFactor_radial_le line 20
  4. def OAI.DefocusingNLS.expandingOrderedDifference line 34
  5. theorem OAI.DefocusingNLS.expandingOrderedDifference_high line 39