OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousOrderedDerivatives.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Ordered Cartesian derivatives and the high homogeneous energy

The sum over all ordered k-tuples of Cartesian directions is exactly the Fourier weight |ξ|^(2k). This supplies the high-energy interpretation needed to apply one pointwise principal potential to each derivative component.

  1. def OAI.DefocusingNLS.homogeneousOrderedDerivative line 20
  2. theorem OAI.DefocusingNLS.radianFourierKernel_iteratedLineDeriv line 24
  3. theorem OAI.DefocusingNLS.homogeneousOrderedDerivative_fourier line 36
  4. theorem OAI.DefocusingNLS.homogeneousOrderedDerivative_fourier_sum line 44
  5. theorem OAI.DefocusingNLS.integrable_schwartz_norm_sq line 62
  6. theorem OAI.DefocusingNLS.homogeneousOrderedDerivative_energy line 66