OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousGluedAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The regular spectral average preserves every finite order at the origin.

  1. theorem OAI.DefocusingNLS.homogeneousGlued_average_contDiffOn line 12
  2. theorem OAI.DefocusingNLS.homogeneousGlued_origin_smooth line 38