OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzProfileSampling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform expanding-torus bound for the entire cutoff profile

Only finitely many symbol derivatives are required. The proof includes the compact core, all inner dyadic annuli, and the final outer annulus.

  1. theorem OAI.DefocusingNLS.outer_annulus_decay line 18
  2. theorem OAI.DefocusingNLS.exists_cutoffProfile_sampling_bound line 30