OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffAnnulusUniform.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform norm bounds for every annulus of the physical cutoff profile

  1. theorem OAI.DefocusingNLS.cutoffOuterAnnulus_decay line 13
  2. theorem OAI.DefocusingNLS.exists_cutoffAnnulus_uniform_bound line 23