OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralContinuousMultiplier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous coefficients on the fixed ball, with their actual L² multipliers and the operator-norm consequence of uniform convergence.

  1. def OAI.DefocusingNLS.spectralContinuousCoefficient line 11
  2. theorem OAI.DefocusingNLS.spectralContinuousCoefficient_density line 17
  3. theorem OAI.DefocusingNLS.spectralContinuousCoefficient_bound line 20
  4. theorem OAI.DefocusingNLS.spectralContinuousMultiplier_tendsto line 26