OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingEnergyScaling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of the two expanding-torus energies

  1. theorem OAI.DefocusingNLS.expandingRadius_rpow line 9
  2. theorem OAI.DefocusingNLS.expandingScaleRatio_sq line 17
  3. theorem OAI.DefocusingNLS.expandingLowFraction_transport line 26
  4. theorem OAI.DefocusingNLS.expandingHighFraction_transport line 40
  5. theorem OAI.DefocusingNLS.expandingFreeStep_mode_norm_sq line 54
  6. theorem OAI.DefocusingNLS.expandingLowEnergy_free line 71
  7. theorem OAI.DefocusingNLS.expandingHighEnergy_free line 91
  8. theorem OAI.DefocusingNLS.expandingFreeEnergy_norm_sq line 111