OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralSmoothHarmonicBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform C1 control on the ball bounds the completed harmonic energy.

  1. theorem OAI.DefocusingNLS.spectralHarmonicNorm_le_sum line 11
  2. theorem OAI.DefocusingNLS.spectralSmoothHarmonic_uniform_bound line 24