OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEssentialContraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual time-step contraction on weakly null data

The integrated local term tends to zero by the already proved compact physical observation. This is the whole-space time-step estimate used before the finite-rank spectral decomposition.

  1. theorem OAI.DefocusingNLS.homogeneousLinearized_weakNull_contraction line 19