Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Simultaneous Diagonalization o...


view this post on Zulip Email Gateway (Aug 16 2022 at 15:11):

From: Manuel Eberl <manuel@pruvisto.org>
Simultaneous Diagonalization of Pairwise Commuting Hermitian Matrices

Mnacho Echenim

A Hermitian matrix is a square complex matrix that is equal to its
conjugate transpose. The (finite-dimensional) spectral theorem states
that any such matrix can be decomposed into a product of a unitary
matrix and a diagonal matrix containing only real elements. We formalize
the generalization of this result, which states that any finite set of
Hermitian and pairwise commuting matrices can be decomposed as
previously, using the same unitary matrix; in other words, they are
simultaneously diagonalizable. Sets of pairwise commuting Hermitian
matrices are called /Complete Sets of Commuting Observables/ in Quantum
Mechanics, where they represent physical quantities that can be
simultaneously measured to uniquely distinguish quantum states.

https://www.isa-afp.org/entries/Commuting_Hermitian.html

Enjoy!


Last updated: Apr 24 2024 at 16:18 UTC