OAI/MathematicalPhysics/DefocusingNLS/Linear/TorusOddCommutator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full physical odd-power commutator has uniform high-frequency gain

  1. theorem OAI.DefocusingNLS.torusOddCommutator_identification line 16
  2. theorem OAI.DefocusingNLS.exists_torusOddCommutator_high_bound line 37