OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzPeriodization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform periodization bounds for the localization kernel

Fourteen powers of decay suffice in twelve dimensions. Lattice translation reduces each continuous frequency to a bounded fundamental cell, and the already proved lattice p-series controls the remaining sum.

  1. theorem OAI.DefocusingNLS.schwartz_decay_fourteen line 17
  2. theorem OAI.DefocusingNLS.bounded_shift_decay line 30
  3. theorem OAI.DefocusingNLS.summable_localization_majorant line 59
  4. theorem OAI.DefocusingNLS.exists_schwartz_periodization_bound line 67

    Source documentation

    Every Schwartz localization kernel has a uniform lattice-periodization bound.

    theorem exists_schwartz_periodization_bound (K : 𝓢(EuclideanSpace ℝ (Fin 12), ℂ)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (S : Finset frequencyLattice) (x : EuclideanSpace ℝ (Fin 12)),
      ∑ n ∈ S, ‖K (x - n)‖ ≤ C := by
…

    Mentions: OAI.DefocusingNLS.frequencyLattice