Kraus update, POVM elements, density matrices, and complete positivity

Definition

PeresTerno_kraus_basics

by Lucas · 1 vote · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

kraus-operatorsquantum-information

Let $d$ , $e$ be finite index sets and let $\{A_m\}_{m\in I}$ be a finite family of complex $e\times d$ matrices (the Kraus matrices of one outcome). This file defines:

the Kraus update of a $d\times d$ matrix $\rho$ (Eq. (6)):

\rho' = \sum_{m\in I} A_m\,\rho\,A_m^\dagger \quad (\text{an } e\times e \text{ matrix});

the POVM element (Eq. (8)):

E = \sum_{m\in I} A_m^\dagger A_m \quad (\text{a } d\times d \text{ matrix, the size of the initial state});

a density matrix: a positive semidefinite complex matrix of trace $1$ ;
the ampliation $T\otimes\mathbb 1$ of a map $T$ from $d\times d$ to $e\times e$ matrices, acting on a matrix $R$ indexed by $d\times F$ by applying $T$ to every $d\times d$ block $(R_{(i,a),(j,b)})_{i,j}$ ;
a positive map: $T(\rho)$ is positive semidefinite whenever $\rho$ is;
a completely positive map: $(T\otimes\mathbb 1)(R)$ is positive semidefinite for every positive semidefinite $R$ on $\mathbb C^d\otimes\mathbb C^n$ , for every $n\in\mathbb N$ .

These are the shared vocabulary of every statement in the mission.

Formalization Note The maps in items 4-6 are arbitrary functions on matrices (linearity is required separately where the source requires it). The ancilla in item 6 is indexed by Fin n.

Definition code

import Mathlib

/-!
# Kraus operators, POVM elements, and complete positivity

Definitions for the mission drafted from A. Peres and D. R. Terno,
*Quantum information and relativity theory*, Rev. Mod. Phys. 76 (2004) 93,
Sec. II.D–II.E, Eqs. (6)–(11).
-/

namespace PeresTerno

open Matrix
open scoped ComplexOrder

/-- Eq. (6): the (unnormalized) post-measurement state
`ρ'_μ = ∑ₘ A_{μm} ρ A_{μm}†` for the Kraus matrices `A m` of one outcome `μ`.
The Kraus matrices may change the dimension (`e × d`). -/
noncomputable def krausUpdate {d e ι : Type*} [Fintype d] [Fintype ι]
    (A : ι → Matrix e d ℂ) (ρ : Matrix d d ℂ) : Matrix e e ℂ :=
  ∑ m, A m * ρ * (A m)ᴴ

/-- Eq. (8): the POVM element `E_μ = ∑ₘ A_{μm}† A_{μm}` (a `d × d` matrix, the same size
as the initial state). -/
noncomputable def povmElement {d e ι : Type*} [Fintype e] [Fintype ι]
    (A : ι → Matrix e d ℂ) : Matrix d d ℂ :=
  ∑ m, (A m)ᴴ * A m

/-- A density matrix: positive semidefinite with unit trace. -/
def IsDensityMatrix {d : Type*} [Fintype d] (ρ : Matrix d d ℂ) : Prop :=
  ρ.PosSemidef ∧ ρ.trace = 1

/-- The map `T ⊗ 1` acting on a bipartite matrix on `d × f`: `T` is applied to each
`d × d` block `(R_{(i,a),(j,b)})_{i,j}` indexed by the ancilla labels `a, b`. -/
def ampliate {d e f : Type*} (T : Matrix d d ℂ → Matrix e e ℂ)
    (R : Matrix (d × f) (d × f) ℂ) : Matrix (e × f) (e × f) ℂ :=
  fun p q => T (fun i j => R (i, p.2) (j, q.2)) p.1 q.1

/-- A map is positive if it sends positive semidefinite matrices to positive semidefinite
matrices. -/
def IsPositiveMap {d e : Type*} [Fintype d] [Fintype e]
    (T : Matrix d d ℂ → Matrix e e ℂ) : Prop :=
  ∀ ρ : Matrix d d ℂ, ρ.PosSemidef → (T ρ).PosSemidef

/-- A map is completely positive if `T ⊗ 1` is positive for an ancilla of every finite
dimension `n`. -/
def IsCompletelyPositive {d e : Type*} [Fintype d] [Fintype e]
    (T : Matrix d d ℂ → Matrix e e ℂ) : Prop :=
  ∀ (n : ℕ) (R : Matrix (d × Fin n) (d × Fin n) ℂ), R.PosSemidef →
    (ampliate T R).PosSemidef

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, pp. 99-100, Sec. II.D, Eqs. (6) and (8); complete positivity as defined on p. 100

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.

The file declares, inside a namespace PeresTerno, the following objects; all matrices have complex entries and all index types used in sums are finite.

Kraus update. For index types $d, e$ ( $d$ finite), a finite index type $I$ , a family $A : I \to \mathbb C^{e\times d}$ and a $d\times d$ matrix $\rho$ , the $e\times e$ matrix

\mathrm{krausUpdate}(A,\rho) = \sum_{m\in I} A_m\,\rho\,A_m^{\dagger},

where ${}^\dagger$ is the conjugate transpose. If $I$ is empty this is the zero matrix.

POVM element. For $e$ finite and $A$ as above, the $d\times d$ matrix

\mathrm{povmElement}(A) = \sum_{m\in I} A_m^{\dagger} A_m ,

zero if $I$ is empty.

Density matrix. For a finite index type $d$ , a $d\times d$ matrix $\rho$ is a density matrix iff $\rho$ is positive semidefinite (Hermitian with $x^\dagger \rho x \ge 0$ for all $x$ ) and $\operatorname{tr}\rho = 1$ . If $d$ is empty no matrix qualifies (its trace is $0$ ).
Ampliation. For any function $T$ from $d\times d$ matrices to $e\times e$ matrices (no linearity assumed) and any matrix $R$ indexed by pairs in $d\times F$ , the matrix indexed by $e\times F$ whose entry at row $(k,a)$ , column $(l,b)$ is

\big[T\big(R^{(a,b)}\big)\big]_{k l}, \qquad R^{(a,b)}_{ij} = R_{(i,a),(j,b)} .

Positive map. For finite $d, e$ , $T$ is positive iff for every positive semidefinite $d\times d$ matrix $\rho$ , $T(\rho)$ is positive semidefinite.
Completely positive map. For finite $d, e$ , $T$ is completely positive iff for every natural number $n$ (including $n=0$ ) and every positive semidefinite matrix $R$ indexed by $d\times\{0,\dots,n-1\}$ , the ampliation of $T$ applied to $R$ (item 4) 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).
Endorsed by Alien60 · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph