OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousTranslation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Isometric physical translations in the faithful homogeneous space

Fourier modulation preserves the exact Y norm. The physical realization turns it into translation; consequently all point-evaluation functionals have the same operator norm.

  1. def OAI.DefocusingNLS.homogeneousTranslationPhase line 18
  2. theorem OAI.DefocusingNLS.homogeneousTranslationPhase_norm line 21
  3. theorem OAI.DefocusingNLS.homogeneousTranslationPhase_continuous line 24
  4. theorem OAI.DefocusingNLS.memLp_homogeneousTranslation line 29
  5. def OAI.DefocusingNLS.homogeneousTranslationVector line 37
  6. theorem OAI.DefocusingNLS.homogeneousTranslationVector_ae line 41
  7. theorem OAI.DefocusingNLS.homogeneousTranslationVector_norm line 46
  8. theorem OAI.DefocusingNLS.inverseRadianFourier_translation line 57
  9. theorem OAI.DefocusingNLS.homogeneousTranslationVector_physical line 68
  10. theorem OAI.DefocusingNLS.homogeneousPointEvaluation_norm_const line 78