OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRegularWeighted.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A Gaussian weight makes the regular-origin Volterra operator contractive on any finite radius.

  1. theorem OAI.DefocusingNLS.spectralRegularAverage_weighted_bound line 11
  2. theorem OAI.DefocusingNLS.integral_mul_exp_square line 22
  3. theorem OAI.DefocusingNLS.spectralRegularPrimitive_weighted_bound line 35