OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzSeparatedPeriodization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Disjointness of sufficiently separated compactly supported translates

  1. theorem OAI.DefocusingNLS.norm_tsum_sq_of_atMostOne line 13
  2. theorem OAI.DefocusingNLS.separatedSchwartz_atMostOne line 26
  3. theorem OAI.DefocusingNLS.separatedSchwartz_norm_tsum_sq line 42