OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzOuterAnnulusSampling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The outer annulus in the uniform cutoff estimate

The radius-R annulus with L ≤ R ≤ 2L is reduced to a bounded dilation at effective period one. This covers the final annulus in a dyadic decomposition.

  1. theorem OAI.DefocusingNLS.exists_outerSchwartzDilation_sampling_bound line 18
  2. def OAI.DefocusingNLS.schwartzDoubleScale line 53
  3. theorem OAI.DefocusingNLS.schwartzDoubleScale_apply line 57
  4. theorem OAI.DefocusingNLS.cutoffProfileAnnulus_outer_rescale line 60
  5. theorem OAI.DefocusingNLS.exists_outerCutoffAnnulus_sampling_bound line 74