OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSchwartzObservation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The compact low-energy part of a Schwartz coefficient

On the dense physical Schwartz domain, multiplication by a fixed Schwartz coefficient takes bounded weakly null data to zero in the exact low energy. The proof combines physical L² observation, Plancherel and frequency splitting.

  1. theorem OAI.DefocusingNLS.homogeneousYProduct_physicalSchwartz line 23
  2. theorem OAI.DefocusingNLS.schwartz_frequency_integrable line 37
  3. theorem OAI.DefocusingNLS.homogeneousLowEnergy_schwartz_interpolation line 47