OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPhysicalDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded physical ordered derivatives on the faithful Y completion

Each ordered top derivative is a bounded map into physical L², with norm at most one. On the dense Schwartz domain it is the usual Cartesian derivative.

  1. def OAI.DefocusingNLS.homogeneousOrderedDerivativeL2 line 19
  2. theorem OAI.DefocusingNLS.homogeneousOrderedDerivativeL2_norm_sq line 25
  3. theorem OAI.DefocusingNLS.homogeneousOrderedDerivativeL2_norm_le line 38
  4. def OAI.DefocusingNLS.homogeneousPhysicalDerivative line 57
  5. theorem OAI.DefocusingNLS.homogeneousPhysicalDerivative_Schwartz line 63
  6. theorem OAI.DefocusingNLS.homogeneousPhysicalDerivative_norm_le line 72