OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingLocalConvergence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local uniform convergence of the actual expanding-torus functions

Once the radii diverge, a cutoff that equals one near the origin disappears from every fixed physical ball. The weak localization limit then gives uniform convergence of the original torus functions on that ball.

  1. theorem OAI.DefocusingNLS.eventually_expandingCutoff_one line 19
  2. theorem OAI.DefocusingNLS.expandingTorus_local_uniform_of_localized_weak line 34
  3. theorem OAI.DefocusingNLS.exists_expandingTorus_local_limit line 68