OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffResidualCoefficients.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Compact annular coefficients of the cutoff residual

  1. def OAI.DefocusingNLS.cutoffGradientCoefficient line 15
  2. theorem OAI.DefocusingNLS.cutoffGradientCoefficient_apply line 19
  3. def OAI.DefocusingNLS.cutoffLaplacianCoefficient line 23
  4. theorem OAI.DefocusingNLS.cutoffLaplacianCoefficient_apply line 26
  5. def OAI.DefocusingNLS.cutoffPowerCoefficient line 31
  6. theorem OAI.DefocusingNLS.cutoffPowerCoefficient_apply line 36
  7. theorem OAI.DefocusingNLS.tsupport_annulus_of_zero line 40
  8. theorem OAI.DefocusingNLS.cutoff_eventually_constant line 55
  9. theorem OAI.DefocusingNLS.cutoffGradientCoefficient_annulus line 68
  10. theorem OAI.DefocusingNLS.cutoffLaplacianCoefficient_annulus line 79
  11. theorem OAI.DefocusingNLS.cutoffPowerCoefficient_annulus line 90
  12. theorem OAI.DefocusingNLS.hasCompactSupport_of_cutoff_annulus line 102