OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLowCompact.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact low-order action of a fixed physical coefficient

The frequency interpolation inequality extends from Schwartz functions to the faithful completion, using the actual weighted physical L² observation. Consequently the low Sobolev part of multiplication by a fixed Schwartz coefficient vanishes on every bounded weakly null sequence.

  1. theorem OAI.DefocusingNLS.homogeneousLowEnergy_coefficient_interpolation line 20
  2. theorem OAI.DefocusingNLS.tendsto_homogeneousLowEnergy_schwartzCoefficient line 39