OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingOrderedCommutator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact principal and commutator splitting of the torus linearization

The remainder below is formed from the actual odd-power derivative and the actual physical Fourier derivative components. Its definition adds no spectral or compactness assumption.

  1. def OAI.DefocusingNLS.expandingLinearizedPotential line 23
  2. def OAI.DefocusingNLS.expandingOrderedCommutator line 28
  3. theorem OAI.DefocusingNLS.expandingOrderedCommutator_split line 39
  4. theorem OAI.DefocusingNLS.expandingLinearized_energy_split line 54
  5. theorem OAI.DefocusingNLS.expandingLinearized_energy_le line 75