Lemma: Insertion wavefront bound

For every $\alpha$,

For a finite normal-jet sum, the corresponding union is a wavefront upper bound.

Proof. The tensor product $b(s)\otimes {\delta }^{(5)}(n)$ is defined. Its tensor-product wavefront bound is exactly the inclusion in (eq:liftcone), with zero covectors adjoined on the supports. Normal differentiation does not enlarge this bound. Finite sums preserve the asserted upper bound Hormander (Section 8.2).