OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRadialDominatingWeight.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An integrable bound for the squared positive-radius evaluation norm.

  1. theorem OAI.DefocusingNLS.spectral_radial_inverse_tenth_integrable line 11
  2. def OAI.DefocusingNLS.spectralRadialEvaluationWeight line 26
  3. theorem OAI.DefocusingNLS.spectralRadialEvaluationWeight_integrable line 29
  4. theorem OAI.DefocusingNLS.spectralRadialPointValue_sq_bound line 33
  5. theorem OAI.DefocusingNLS.spectralRadialSmooth_sq_bound line 54