OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEvaluationContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Norm-continuity of actual point observation

The Fourier translation isometry makes all evaluation dual norms equal. Physical continuity gives weak continuity of their Riesz vectors; the constant norm and the Hilbert norm-square identity give norm-continuity.

  1. theorem OAI.DefocusingNLS.continuous_homogeneousPointEvaluation line 19