OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzAnnulusSampling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform sampling of physical symbol annuli

The Fourier sample of a physical radius-R annulus has norm O(R^(-a)), uniformly for L ≥ R. The constant uses finitely many symbol derivatives.

  1. def OAI.DefocusingNLS.schwartzPhysicalDilation line 18
  2. theorem OAI.DefocusingNLS.schwartzPhysicalDilation_apply line 24
  3. theorem OAI.DefocusingNLS.radianFourierKernel_schwartzPhysicalDilation line 30
  4. theorem OAI.DefocusingNLS.schwartzPhysicalDilation_annulus line 50
  5. theorem OAI.DefocusingNLS.exists_schwartzAnnulusSample_bound line 58