OAI/MathematicalPhysics/DefocusingNLS/Linear/TorusFourierIsometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The physical L² realization of the frequency lattice

Reindexing the existing torus Fourier Hilbert basis gives an exact isometry from the Euclidean lattice model into physical torus L².

  1. def OAI.DefocusingNLS.torusLatticeBasis line 21
  2. theorem OAI.DefocusingNLS.torusLatticeBasis_apply line 33
  3. def OAI.DefocusingNLS.torusFourierIsometry line 38
  4. theorem OAI.DefocusingNLS.torusFourierIsometry_coefficient line 41
  5. theorem OAI.DefocusingNLS.torusFourierIsometry_eq_continuous line 48