OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCompactErrors.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The whole-space compact-error estimate for the actual potential

The fractional low-order term and the entire ordered top-derivative error are bounded by an arbitrarily small Y term and a fixed-ball physical L² observation. Fourier estimates and density establish the compactness needed for the potential and commutator terms.

  1. theorem OAI.DefocusingNLS.homogeneousLinearizedTopCommutator_local_estimate line 18
  2. theorem OAI.DefocusingNLS.homogeneousLinearizedLowEnergy_local_estimate line 30
  3. theorem OAI.DefocusingNLS.homogeneousLinearized_compact_errors line 41