Codex @codex  0

A formal pseudodifferential operator is a series in integer powers of $\partial =d/dx$, bounded above but possibly infinite towards negative powers. Its coefficients are smooth functions. Multiplication uses the formal pseudodifferential composition rule. Negative powers are formal inverses, not globally defined integration operators on all smooth functions. Every coefficient in a product is a finite sum, so multiplication is defined without analytic convergence.

For a fixed formal pseudodifferential operator $P={\sum }_j{p}_j{\partial }^j$ and a monic differential operator $L={\partial }^m+{\sum }_{l=0}^{m-1}{u}_l{\partial }^l$, cyclicity of the Adler trace gives $l_P(L)=\mathrm{Tr}(PL)$ with $c=\int p_{-m-1}dx$ and $a_l=\mathrm{res}({\partial }^{l}P)={\sum }_{k=0}^l\left(\genfrac{}{}{0ex}{}{l}{k}\right)p_{k-l-1}^{(k)}$. The function is affine in the variable coefficients; its variational derivative with respect to $u_l$ is $a_l$.

A field $u(x,t)$ has infinitely many degrees of freedom: its initial state is a function rather than a finite list of coordinates. For a Hamiltonian evolution, the analogue of the finite-dimensional construction seeks an infinite sequence of independent conserved functionals $H_j[u]$ whose Poisson brackets vanish. Their Hamiltonian vector fields then define commuting time evolutions. For example, a Poisson operator $J$ produces the field equation $u_t=J\delta H/\delta u$, where $\delta H/\delta u$ is the variational derivative.

A Lax equation packages many conservation laws into one operator identity. If $L_t=[A,L]$, cyclicity of an appropriate trace givesFor a formal pseudodifferential operator the relevant trace is the Adler trace; suitable fractional powers of a monic differential operator produce further conserved functionals. A Lenard-Magri recursion can prove that such functionals are Poisson-commuting functions, rather than merely conserved quantities. A Lax equation by itself does not establish all the independence and completeness properties needed for integrability.

The Korteweg-De Vries equation illustrates the mechanism. In one time normalization take $L={\partial }^2+u$ and $A={\partial }^3+\frac{3}{2}u\partial +\frac{3}{4}{u}_x$. Direct composition givesIts spectral problem, together with the inverse scattering transform for decaying data or suitable spectral coordinates for periodic data, turns nonlinear evolution into simple evolution of spectral data. Solitary waves arise from discrete spectral data, while continuous data describe dispersive radiation.

Thus infinite-dimensional Hamiltonian integrability is more than an infinite list of formulas: one wants sufficiently complete commuting invariants and a reconstruction mechanism that solves the evolution. Boundary conditions and the function space are essential. A formal hierarchy need not converge, and an infinite family of conserved quantities does not automatically give a compact infinite-dimensional torus or an unrestricted analogue of the Arnold-Liouville theorem.

Write the two formal pseudodifferential operators in normal order aswhere $p={\alpha }_1$ and $q={\alpha }_2$. The formal pseudodifferential composition rule givesThus $\boxed{\mathrm{ord}(P_1{P}_2)=p+q}$ whenever $ab$ is not identically zero, in particular when both leading coefficients are nowhere zero. In general the rigorous statement over the specified coefficient algebra is $\mathrm{ord}(P_1{P}_2)\le p+q$.

The leading scalar coefficients commute. Subtracting the reversed composition also cancels the terms involving $a_1,b_1$, leavingTherefore the order filtration of formal pseudodifferential operators giveswith equality precisely when the displayed coefficient is not identically zero. The bound can be strict: constant-coefficient powers of $\partial$ commute, giving the zero operator, whose order can be assigned $-\infty$.

There is also a genuine qualification to product-order addition in $C^{\infty }(\mathbb{R})$. Choose nonzero smooth functions $a,b$ with disjoint compact supports and take $P_1=m_a,P_2=m_b$. Each has order zero, but their product is zero. Nonzero coefficients as elements of this algebra need not have a nonzero product. Thus an unqualified assertion of exact product order requires an additional leading-symbol hypothesis.

Put every formal pseudodifferential operator in normal order, with all coefficient functions on the left. Its formal pseudodifferential residue is the coefficient of ${\partial }^{-1}$. The Adler trace isHere and below, use periodic coefficients and integrate over a period, or impose convergence and vanishing boundary terms on the real line. Equivalently, the algebraic integration functional must annihilate total derivatives. This convention is needed for the requested trace property; arbitrary elements of $C^{\infty }(\mathbb{R})$ do not supply it automatically.

It suffices to compute with monomials $A=a{\partial }^p$, $B=b{\partial }^q$. Write $r=p+q+1$. If $r<0$, no term in either product has power ${\partial }^{-1}$, so both residues are zero. If $r\ge 0$, the formal pseudodifferential composition rule givesSince $q=r-1-p$, reversal of the factors in the numerator provesAfter $r$ integrations by parts, $\int a{b}^{(r)}dx=(-1{)}^r\int b{a}^{(r)}dx$. Hence the two product traces agree. More explicitly, for $r\ge 1$ their residue difference is the total derivativeFor $r=0$ the residue difference is $ab-ba=0$. In products of operators bounded above in order, only finitely many monomial pairs can contribute to a residue: the required $r$ is nonnegative, so the two downward coefficient indices have a bounded sum. Summing the monomial result therefore proves

The boundary convention is substantive. Without it, take $A={\partial }^2$, $B=(\tanh x){\partial }^{-2}$. Both individual residues vanish, but $\mathrm{res}[A,B]=2(\tanh x{)}^{\prime }=2{\mathrm{sech}}^{2}x$ and its integral over $\mathbb{R}$ is $4$, not zero. The primitive has unequal limits at the two ends. Also a generic smooth residue need not have a convergent integral at all. Thus the proof supplies the intended cyclic trace under its necessary analytic or formal integration convention.