OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzPeriodizationIntegral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Integration of the genuine lattice periodization

The fundamental-cell integral of a periodized Schwartz function, twisted by a periodic unit-modulus character, is its whole-space integral.

  1. instance OAI.DefocusingNLS.frequencyLattice_vaddInvariant_volume line 20
  2. def OAI.DefocusingNLS.frequencyCell line 26
  3. theorem OAI.DefocusingNLS.frequencyCell_isAddFundamentalDomain line 29
  4. theorem OAI.DefocusingNLS.frequencyCell_isBounded line 33
  5. theorem OAI.DefocusingNLS.frequencyCell_measurableSet line 36
  6. theorem OAI.DefocusingNLS.frequencyCell_volume_lt_top line 39
  7. theorem OAI.DefocusingNLS.schwartzPeriodization_twisted_integral line 42
  8. theorem OAI.DefocusingNLS.schwartzPeriodization_integral line 82