OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPhysicalKernelDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Differentiating the exact physical free kernel

The estimates are on the scalar kernel itself. They require only the second Fourier moment, already proved for every vector in the manuscript's Y space.

  1. def OAI.DefocusingNLS.homogeneousPhysicalFreeKernelDerivative line 19
  2. theorem OAI.DefocusingNLS.physicalPhase_hasDerivAt line 24
  3. theorem OAI.DefocusingNLS.homogeneousPhysicalFreeKernel_norm line 37
  4. theorem OAI.DefocusingNLS.hasDerivAt_homogeneousPhysicalFreeKernel line 43
  5. theorem OAI.DefocusingNLS.homogeneousPhysicalFreeKernelDerivative_norm_le line 53
  6. theorem OAI.DefocusingNLS.homogeneousPhysicalFreeKernelDerivative_local_bound line 77