The question of solvability

We give a proof of the Nirenberg-Treves conjecture: that local solvability of principal type pseudodifferential operators is equivalent to condition (Psi). This condition rules out sign changes from - to + of the imaginary part of the principal symbol along the oriented bicharacteristics of the real part. We obtain local solvability by proving a localizable a priori estimate for the adjoint operator with a loss of two derivatives (compared with the elliptic case)