OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzLocalConvolution.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Smooth spatial filtering preserves local uniform limits

A globally bounded sequence that vanishes locally uniformly also vanishes, on every fixed ball, after convolution by a Schwartz kernel. The proof uses the compact-ball Banach space, so the conclusion is uniform in space.

  1. def OAI.DefocusingNLS.shiftedBallRestriction line 20
  2. theorem OAI.DefocusingNLS.shiftedBallRestriction_apply line 25
  3. theorem OAI.DefocusingNLS.continuous_shiftedBallRestriction line 28
  4. theorem OAI.DefocusingNLS.shiftedBallRestriction_norm_le line 33
  5. def OAI.DefocusingNLS.schwartzBallConvolution line 39
  6. theorem OAI.DefocusingNLS.schwartzBallConvolution_integrable line 43
  7. theorem OAI.DefocusingNLS.schwartzBallConvolution_apply line 53
  8. theorem OAI.DefocusingNLS.tendsto_schwartzBallConvolution_zero line 61
  9. theorem OAI.DefocusingNLS.schwartzBallConvolution_sub line 96
  10. theorem OAI.DefocusingNLS.tendsto_schwartzBallConvolution line 110