Lemma 2.30 — positive operators supported on a matrix range

Open

WatrousTQI.psd_supported_factorization

by Mrnaiq · Nov 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexitykraus-operatorsprove2quantumquantum-channels

For arbitrary positive dimensions $n,m$ , any complex $n\times m$ matrix $A$ , and any complex $n\times n$ matrix $P$ ,

P\succeq0\ \text{and}\ \operatorname{im}P\subseteq\operatorname{im}A\quad\Longleftrightarrow\quad \exists Q\succeq0:\ P=AQA^\dagger.

No injectivity, invertibility, or full-rank hypothesis is imposed on $A$ . This is the range factorization needed to describe positive operators supported on a Choi matrix's support.

Preamble

import Mathlib
set_option autoImplicit false
noncomputable section
open scoped Matrix ComplexConjugate ComplexOrder BigOperators

Formal statement

namespace WatrousTQI
theorem psd_supported_factorization {n m : ℕ} (hn : 0 < n) (hm : 0 < m)
    (A : Matrix (Fin n) (Fin m) ℂ) (P : Matrix (Fin n) (Fin n) ℂ) :
    (P.PosSemidef ∧ LinearMap.range P.mulVecLin ≤ LinearMap.range A.mulVecLin) ↔
      ∃ Q : Matrix (Fin m) (Fin m) ℂ, Q.PosSemidef ∧ P = A * Q * Aᴴ := by sorry
end WatrousTQI

Source

John Watrous, The Theory of Quantum Information, Cambridge University Press, 2018, Section 2.2.4, printed pp.96–99. https://cs.uwaterloo.ca/~watrous/TQI/TQI.pdf; Lemma 2.30, equation (2.171), printed p.96.

Read-back

What the Lean code literally says, in plain math · GPT-6 (exact model identifier unavailable)

For every pair of natural numbers $n,m$ with $0<n$ and $0<m$ , every complex $n\times m$ matrix $A$ , and every complex $n\times n$ matrix $P$ , the following are equivalent: $P$ is positive semidefinite and its column space is contained in the column space of $A$ ; and there exists a complex $m\times m$ positive semidefinite matrix $Q$ such that $P=AQA^*$ . Here $A^*$ is the conjugate transpose, and each column space is the range of the complex-linear map given by matrix multiplication on a column vector. Positive semidefiniteness means Hermitian symmetry together with $x^*Px\geq0$ for every complex column vector $x$ (and likewise for $Q$ ). Both dimensions must be positive, but $A$ may have any rank, including zero, and $P$ may be zero. The existential assertion does not require $Q$ to be positive definite or unique.

View graph