OAI/MathematicalPhysics/DefocusingNLS/Linear/LocalizationFatou.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing the localization energy bound to a Fourier-series limit

Fatou's lemma applies to the nonnegative Fourier energy densities indexed by finite frequency sets. A uniform bound gives integrability of the limit as well as the same numerical energy bound.

  1. theorem OAI.DefocusingNLS.localization_integral_limit line 18