Simultaneous Williamson's normal form for positive operators

We prove a simultaneous Williamson’s normal form for two symplectically commuting positive operators $A,B$ on a real symplectic Hilbert space $(\mathbf{H},J)$. Under a natural commutativity condition, there exists a (generally unbounded) operator $\mathrm{\Phi }$ that simultaneously diagonalizes $A$ and $B$ in the symplectic setting as $A={\mathrm{\Phi }}^t{M}_A\mathrm{\Phi }$, $B={\mathrm{\Phi }}^t{M}_B\mathrm{\Phi }$, and maps $J$ to a canonical symplectic operator. The result generalizes Williamson’s normal form to infinite dimensions and yields a complete spectral invariant for the pair $(A,B)$.