OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzTorusSampling.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Schwartz Fourier sampling in the exact expanding-torus space

The sampled coefficients carry the physical volume factor (2πL)⁻¹². Their exact Y_L vectors have norms bounded independently of L ≥ 1.

  1. def OAI.DefocusingNLS.schwartzLatticeCoefficient line 18
  2. def OAI.DefocusingNLS.weightedSchwartzLatticeCoefficient line 22
  3. theorem OAI.DefocusingNLS.weightedSchwartzLatticeCoefficient_norm_sq line 26
  4. theorem OAI.DefocusingNLS.sampling_density_le line 50
  5. theorem OAI.DefocusingNLS.exists_weightedSchwartz_torus_sampling_bound line 71
  6. def OAI.DefocusingNLS.schwartzTorusSample line 112
  7. theorem OAI.DefocusingNLS.schwartzTorusSample_coefficient line 119
  8. theorem OAI.DefocusingNLS.exists_schwartzTorusSample_norm_bound line 129
  9. theorem OAI.DefocusingNLS.schwartzTorusSample_function line 145