OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFiniteCodimension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite-dimensional exception to the actual weak-null contraction

The argument uses a countable dense family only to choose finitely many orthogonality constraints. The weak-null bound is supplied by the proved whole-space energy observation inequality.

  1. theorem OAI.DefocusingNLS.homogeneousOperator_finite_annihilator line 18