OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingFilteredDerivatives.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Ordered frequency derivatives of the compactly filtered torus field

  1. def OAI.DefocusingNLS.smoothDerivativeKernel line 15
  2. theorem OAI.DefocusingNLS.smoothDerivativeKernel_fourier line 19
  3. def OAI.DefocusingNLS.expandingSmoothDerivative line 27
  4. theorem OAI.DefocusingNLS.expandingSmoothDerivative_apply line 31
  5. theorem OAI.DefocusingNLS.expandingSmoothDerivative_physical line 38
  6. theorem OAI.DefocusingNLS.expandingSmoothDerivative_physical_bound line 46
  7. theorem OAI.DefocusingNLS.tendsto_expandingSmoothDerivative_local line 60