OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousTopCommutator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual top-order commutator on the faithful homogeneous space

This is the difference between differentiating the physical product and multiplying the physical derivative. Its coefficient dependence is bounded in the Y norm, allowing approximation of the actual profile coefficients.

  1. def OAI.DefocusingNLS.homogeneousTopCommutatorValue line 21
  2. theorem OAI.DefocusingNLS.homogeneousTopCommutatorValue_norm_le line 27
  3. def OAI.DefocusingNLS.homogeneousTopCommutator line 48
  4. theorem OAI.DefocusingNLS.homogeneousTopCommutator_apply line 65
  5. theorem OAI.DefocusingNLS.homogeneousTopCommutator_Schwartz line 71