OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCommutatorSymbol.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One frequency gain in the actual ordered derivative commutator

The difference of the two ordered Fourier symbols loses one power of the large frequency. This is the algebraic input for the high-energy compact commutator; no compactness or operator estimate is assumed here.

  1. def OAI.DefocusingNLS.homogeneousOrderedSymbol line 16
  2. theorem OAI.DefocusingNLS.homogeneousOrderedSymbol_norm_le line 19
  3. theorem OAI.DefocusingNLS.homogeneousOrderedSymbol_sub_le line 30
  4. theorem OAI.DefocusingNLS.homogeneousOrderedSymbol_highFrequency line 75