Eq. (8): POVM elements $E=\sum_m A_m^\dagger A_m$ are positive

Proved

PeresTerno.povmElement_posSemidef

by Lucas · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

quantum-information

Let $\{A_m\}_{m\in I}$ be a finite family of complex $e\times d$ matrices. Then the $d\times d$ matrix

E = \sum_{m\in I} A_m^\dagger A_m

is positive semidefinite.

The source calls the matrices of Eq. (8) "the positive operators $E_\mu$ "; this is the positivity that makes them elements of a POVM.

Preamble

import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

open Matrix
open scoped ComplexOrder

Formal statement

namespace PeresTerno

theorem povmElement_posSemidef {d e ι : Type*} [Fintype d] [Fintype e] [Fintype ι]
    (A : ι → Matrix e d ℂ) :
    (povmElement A).PosSemidef := by
  sorry

end PeresTerno

Source

A. Peres and D. R. Terno, Quantum information and relativity theory, Rev. Mod. Phys. 76, 93-123 (2004), https://doi.org/10.1103/RevModPhys.76.93, p. 100, Sec. II.D, Eq. (8) ("The positive operators E_mu")

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - NON-BLIND: same agent that drafted the statements

Non-blind read-back - not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning, at the explicit request of the proposal owner. It was not produced by a blind, independent auditor and must not be mistaken for independent testimony. Reviewers should compare the Lean code against the source themselves.

For index types $d, e$ (finite) and a finite index type $I$ , and every family $A : I\to\mathbb C^{e\times d}$ , the $d\times d$ matrix $\sum_{m\in I} A_m^{\dagger}A_m$ is positive semidefinite, i.e. it is Hermitian and $x^\dagger\big(\sum_m A_m^\dagger A_m\big)x \ge 0$ for every $x\in\mathbb C^d$ . No hypothesis is placed on $A$ ; for empty $I$ the matrix is $0$ , which is positive semidefinite.

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (8): POVM elements E=∑mAm†AmE=\sum_m A_m^\dagger A_mE=∑m​Am†​Am​ are positive

Eq. (8): POVM elements $E=\sum_m A_m^\dagger A_m$ are positive