OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousComplexDecomposition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Complex finite-rank decomposition from the actual weak-null estimate

Choosing a sufficiently small real remainder absorbs the norm factor in complexification. The only input is the quantitative weak-null estimate already proved for the actual linearized propagator.

  1. theorem OAI.DefocusingNLS.homogeneousOperator_complexFiniteRank_contraction line 16