OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzSamplingDilation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact dilation of the sampled expanding-torus vector

An annulus of physical radius R is sampled at effective period L/R. The canonical scale transfer gives exactly the decay factor R^(-a) for 1 ≤ R ≤ L.

  1. theorem OAI.DefocusingNLS.schwartzLatticeCoefficient_homogeneousDilation line 19
  2. theorem OAI.DefocusingNLS.schwartzTorusSample_homogeneousDilation line 44
  3. theorem OAI.DefocusingNLS.schwartzTorusSample_homogeneousDilation_norm_le line 71