Theorem 2.31 proof — support of positive convex summands

Open

WatrousTQI.psd_convex_summand_range

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

convexitykraus-operatorsprove2quantumquantum-channels

Let $Q_0,Q_1$ be positive semidefinite complex $n\times n$ matrices, $n>0$ , and let $0<t<1$ . If

P=tQ_0+(1-t)Q_1,

then

\operatorname{im}Q_0\subseteq\operatorname{im}P,\qquad\operatorname{im}Q_1\subseteq\operatorname{im}P.

Both coefficients are strictly positive; no invertibility or fixed rank is assumed. This isolates the support-containment step used for Choi matrices of channels in a proper convex decomposition.

Preamble

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

Formal statement

namespace WatrousTQI
theorem psd_convex_summand_range {n : ℕ} (hn : 0 < n)
    (P Q₀ Q₁ : Matrix (Fin n) (Fin n) ℂ)
    (h₀ : Q₀.PosSemidef) (h₁ : Q₁.PosSemidef)
    (t : ℝ) (ht₀ : 0 < t) (ht₁ : t < 1)
    (hP : P = t • Q₀ + (1 - t) • Q₁) :
    LinearMap.range Q₀.mulVecLin ≤ LinearMap.range P.mulVecLin ∧
    LinearMap.range Q₁.mulVecLin ≤ LinearMap.range P.mulVecLin := 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; Proof of Theorem 2.31, equations (2.179)–(2.181), printed p.97; the second inclusion follows by exchanging the two summands.

Read-back

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

For every positive natural number $n$ , all complex $n\times n$ matrices $P,Q_0,Q_1$ , and every real number $t$ , if $Q_0$ and $Q_1$ are positive semidefinite, $0<t<1$ , and $P=tQ_0+(1-t)Q_1$ , then the column space of $Q_0$ is contained in the column space of $P$ and the column space of $Q_1$ is contained in the column space of $P$ . The column space is the range of matrix multiplication as a complex-linear map, and positive semidefiniteness means Hermitian symmetry and nonnegative quadratic form on every complex column vector. The real coefficients act by scalar multiplication on complex matrices. The conclusion is the conjunction of the two inclusions, not equality of any of these spaces. The case $n=0$ and the weights $t=0,1$ are excluded; zero and singular matrices are allowed, and no separate positive semidefiniteness hypothesis is imposed on $P$ beyond the displayed equality and the assumptions on the two summands.

View graph