OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPhysicalGeneratorIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A physical integral formula for the strong free generator

The derivative comes from the actual Fourier representation of the free flow. In particular it applies to the generator vectors selected by the finite spectral contour, with no additional spatial regularity hypothesis.

  1. theorem OAI.DefocusingNLS.continuous_physicalFreeKernel line 20
  2. theorem OAI.DefocusingNLS.continuous_physicalFreeKernelDerivative line 25
  3. theorem OAI.DefocusingNLS.hasDerivAt_homogeneousFree_physical line 32
  4. theorem OAI.DefocusingNLS.homogeneousFree_generator_physical_integral line 82