OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousOutgoingEstimates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded physical derivative rows from the normalized outgoing columns

The radial powers in the value matrix and its inverse cancel. The remaining bound depends only on the bounded normalized jets and inverse.

  1. def OAI.DefocusingNLS.homogeneousPhysicalLogColumn line 19
  2. def OAI.DefocusingNLS.homogeneousNormalizedEulerColumn line 23
  3. theorem OAI.DefocusingNLS.homogeneousNormalizedEulerColumn_bound line 27
  4. theorem OAI.DefocusingNLS.homogeneousPhysicalLogColumn_diagonal line 33
  5. theorem OAI.DefocusingNLS.homogeneousPhysicalLogColumn_euler line 41
  6. theorem OAI.DefocusingNLS.homogeneousOutgoingDerivativeRows_bound line 50