OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFreeEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact free energy rates on the completed space

The low and high squared Sobolev norms acquire the factors exp(-a s) and exp((6-2a-k)s). Density extends the identities from Schwartz data to every element of the faithful Y space.

  1. theorem OAI.DefocusingNLS.homogeneousLowEnergy_free line 17
  2. theorem OAI.DefocusingNLS.homogeneousHighEnergy_free line 37
  3. theorem OAI.DefocusingNLS.homogeneousFreeEnergy_formula line 55
  4. theorem OAI.DefocusingNLS.hasDerivAt_homogeneousFreeEnergy_zero line 63
  5. theorem OAI.DefocusingNLS.homogeneousLowEnergy_free_inner line 80
  6. theorem OAI.DefocusingNLS.homogeneousHighEnergy_free_inner line 93
  7. theorem OAI.DefocusingNLS.homogeneousEnergy_inner line 106