OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingLowPhysicalEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact physical Fourier weight of the lower energy component

  1. theorem OAI.DefocusingNLS.expandingNorm_coordinate_physical line 9
  2. theorem OAI.DefocusingNLS.expandingEnergy_coordinate_split line 23
  3. theorem OAI.DefocusingNLS.expandingLowEnergy_coordinate_physical line 39