OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingCompactEnergyError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact nonprincipal energy error vanishes on locally null sequences

  1. theorem OAI.DefocusingNLS.tendsto_expandingOrderedCommutator line 28
  2. theorem OAI.DefocusingNLS.tendsto_expandingCompactEnergy_error line 41