OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzLatticeSampling.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform sampling of Schwartz Fourier kernels

The normalized sampling sum has a bound independent of the expanding period. The same statement holds with either Sobolev weight.

  1. theorem OAI.DefocusingNLS.schwartz_sampling_decay line 18
  2. theorem OAI.DefocusingNLS.exists_schwartz_scaledLattice_l2_bound line 45
  3. theorem OAI.DefocusingNLS.exists_weightedSchwartz_scaledLattice_l2_bound line 67