OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousProductCompact.lean

Compact low-energy multiplication for every coefficient in Y

Density of physical Schwartz functions in the actual Y norm and the proved bilinear product bound extend the compact observation result to every fixed Y coefficient. This applies to the polynomial coefficients of the actual odd-power linearization.