OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzPeriodizationFunction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual continuous periodization in twelve dimensions

Schwartz decay gives local normal convergence of lattice translates. The resulting function descends to the genuine product torus.

  1. def OAI.DefocusingNLS.frequencyCoordinatesEquiv line 20
  2. theorem OAI.DefocusingNLS.frequencyCoordinatesEquiv_apply line 24
  3. theorem OAI.DefocusingNLS.schwartz_periodization_decay line 27
  4. theorem OAI.DefocusingNLS.schwartz_periodization_translate_bound line 39
  5. def OAI.DefocusingNLS.schwartzLatticeTranslate line 67
  6. theorem OAI.DefocusingNLS.summable_schwartzLatticeTranslate_restrict line 70
  7. theorem OAI.DefocusingNLS.summable_schwartzLatticeTranslate line 91
  8. theorem OAI.DefocusingNLS.summable_norm_schwartz_lattice line 95
  9. def OAI.DefocusingNLS.schwartzPeriodization line 103
  10. theorem OAI.DefocusingNLS.schwartzPeriodization_apply line 106
  11. theorem OAI.DefocusingNLS.schwartzPeriodization_add_lattice line 110
  12. def OAI.DefocusingNLS.unitTorusProjection line 122
  13. theorem OAI.DefocusingNLS.unitTorusProjection_isOpenQuotientMap line 125
  14. theorem OAI.DefocusingNLS.schwartzPeriodization_eq_of_projection_eq line 131
  15. def OAI.DefocusingNLS.schwartzPeriodizedTorus line 153
  16. theorem OAI.DefocusingNLS.schwartzPeriodizedTorus_projection line 166