Gleason's theorem for composite systems

Gleason's theorem [A. Gleason, J. Math. Mech., \textbf{6}, 885 (1957)] is an important result in the foundations of quantum mechanics, where it justifies the Born rule as a mathematical consequence of the quantum formalism. Formally, it presents a key insight into the projective geometry of Hilbert spaces, showing that finitely additive measures on the projection lattice $\PH$ extend to positive linear functionals on the algebra of bounded operators $\BH$. Over many years, and by the effort of various authors, the theorem has been broadened in its scope from type I to arbitrary von Neumann algebras (without type $\text{I}_2$ factors). Here, we prove a generalisation of Gleason's theorem to composite systems. To this end, we strengthen the original result in two ways: first, we extend its scope to dilations in the sense of Naimark [M. A. Naimark, C. R. (Dokl.) Acad. Sci. URSS, n. Ser., \textbf{41}, 359 (1943)] and Stinespring [W. F. Stinespring, Proc. Am. Math. Soc., \textbf{6}, 211 (1955)] and second, we require consistency with respect to dynamical correspondences on the respective (local) algebras in the composition [E. M. Alfsen and F. W. Shultz, Commun. Math. Phys., \textbf{194}, 87 (1998)]. We show that neither of these conditions changes the result in the single system case, yet both are necessary to obtain a generalisation to bipartite systems.