OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousAnnulusBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform Schwartz estimates for normalized annular profile pieces

  1. def OAI.DefocusingNLS.homogeneousAnnulusPiece line 13
  2. theorem OAI.DefocusingNLS.homogeneousAnnulusPiece_apply line 19
  3. theorem OAI.DefocusingNLS.homogeneousAnnulusPiece_rescale line 24
  4. def OAI.DefocusingNLS.homogeneousAnnulusCutoffConstant line 41
  5. theorem OAI.DefocusingNLS.homogeneousAnnulusCutoffConstant_nonneg line 45
  6. def OAI.DefocusingNLS.homogeneousAnnulusJetConstant line 50
  7. theorem OAI.DefocusingNLS.homogeneousAnnulusJetConstant_nonneg line 53
  8. theorem OAI.DefocusingNLS.homogeneousAnnulusPiece_jet_bound line 59