OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzSamplingBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative Schwartz sampling bounds

The constant is independent of both the expanding scale and the Schwartz kernel. Dependence on the kernel is isolated in two weighted decay bounds.

  1. theorem OAI.DefocusingNLS.schwartz_scaledLattice_l2_bound_of_decay line 17
  2. theorem OAI.DefocusingNLS.weightedSchwartz_scaledLattice_bound_of_decay line 53
  3. theorem OAI.DefocusingNLS.schwartzTorusSample_norm_le_of_weighted_decay line 71