OAI/MathematicalPhysics/DefocusingNLS/Linear/TorusOrderedEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Physical ordered components and their principal potential energy

The sum of the squared physical component norms is exactly the high term of Y_L. The leading odd-power action has one bound for every derivative order, using only the profile's pointwise size.

  1. def OAI.DefocusingNLS.expandingOrderedPhysicalEnergy line 22
  2. theorem OAI.DefocusingNLS.expandingOrderedPhysicalEnergy_norm line 27
  3. theorem OAI.DefocusingNLS.expandingOrderedPhysicalEnergy_norm_sq line 33
  4. theorem OAI.DefocusingNLS.expandingOrderedPhysicalEnergy_inner line 39
  5. theorem OAI.DefocusingNLS.expandingOrderedPrincipal_energy_le line 49