OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCommutatorFourier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual ordered derivative commutator in Fourier variables

The kernel contains the difference of the two ordered symbols. Its derivative gain is therefore the proved symbol gain, rather than an assumed commutator estimate.

  1. def OAI.DefocusingNLS.homogeneousOrderedCommutator line 20
  2. theorem OAI.DefocusingNLS.homogeneousOrderedCommutator_fourier line 25