Matrix Sum-of-Squares Helpers #
This module contains finite-dimensional complex matrix lemmas used by the EPR
extraction arguments. It is intentionally concrete over complex matrices: the
proofs use Matrix.dotProduct positivity and conjugate transpose.
theorem
three_selfAdjoint_squares_mulVec_eq_zero
{m : Type u_1}
[Fintype m]
[DecidableEq m]
(T₁ T₂ T₃ : Matrix m m ℂ)
(v : m → ℂ)
(hT₁ : T₁.conjTranspose = T₁)
(hT₂ : T₂.conjTranspose = T₂)
(hT₃ : T₃.conjTranspose = T₃)
(h : (T₁ ^ 2 + T₂ ^ 2 + T₃ ^ 2).mulVec v = 0)
: