Tame Sobolev product estimate ($\Vert fg{\Vert }_{H^k}\lesssim \Vert f{\Vert }_{\infty }\Vert g{\Vert }_{H^k}+\Vert g{\Vert }_{\infty }\Vert f{\Vert }_{H^k}$)

For an integer $k\ge 0$ and sufficiently regular bounded functions, $\Vert fg{\Vert }_{H^k}\le C_k(\Vert f{\Vert }_{\infty }\Vert g{\Vert }_{H^k}+\Vert g{\Vert }_{\infty }\Vert f{\Vert }_{H^k})$. The Leibniz rule and derivative interpolation give the estimate. In a differentiated semilinear wave equation, this separates a controlled low-order coefficient from an arbitrarily high Sobolev norm, allowing propagation of smoothness after a fixed base norm has been controlled.