OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEnergyComponents.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The two exact homogeneous energy components

The low and high Sobolev energies are bounded real-linear observations of the actual weighted Fourier Hilbert space. Their squared norms add to the full Y norm, with the manuscript's Plancherel normalization.

  1. def OAI.DefocusingNLS.homogeneousSobolevWeight line 19
  2. def OAI.DefocusingNLS.homogeneousSobolevMeasure line 22
  3. theorem OAI.DefocusingNLS.homogeneousSobolevWeight_nonneg line 25
  4. theorem OAI.DefocusingNLS.continuous_homogeneousSobolevWeight line 30
  5. theorem OAI.DefocusingNLS.homogeneousFourierMeasure_eq_components line 34
  6. theorem OAI.DefocusingNLS.homogeneousLowMeasure_le line 51
  7. theorem OAI.DefocusingNLS.homogeneousHighMeasure_le line 56
  8. def OAI.DefocusingNLS.homogeneousLowEnergy line 61
  9. def OAI.DefocusingNLS.homogeneousHighEnergy line 66
  10. theorem OAI.DefocusingNLS.homogeneousLowEnergy_ae line 71
  11. theorem OAI.DefocusingNLS.homogeneousHighEnergy_ae line 76
  12. theorem OAI.DefocusingNLS.homogeneousLowEnergy_norm_le line 81
  13. theorem OAI.DefocusingNLS.homogeneousHighEnergy_norm_le line 94
  14. theorem OAI.DefocusingNLS.l2_norm_sq_integral line 107
  15. theorem OAI.DefocusingNLS.homogeneousEnergy_norm_sq line 115
  16. theorem OAI.DefocusingNLS.sobolevEnergy_norm_sq_of_ae line 145
  17. theorem OAI.DefocusingNLS.homogeneousLowEnergy_Schwartz_norm_sq line 161
  18. theorem OAI.DefocusingNLS.homogeneousHighEnergy_Schwartz_norm_sq line 171