Prove2Me

Eqs. (7)-(8): outcome probabilities pμ=tr ρμ′p_\mu=\mathrm{tr}\,\rho'_\mu form a probability distribution

Proved
PeresTerno.outcome_probabilities_distribution

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

quantum-information

Let ρ\rho be a d×dd\times d density matrix, and for each outcome μ\mu in a finite set MM let {Aμm}m∈Iμ\{A_{\mu m}\}_{m\in I_\mu} be a finite family of complex e×de\times d Kraus matrices whose POVM elements are complete:

∑μ∈M∑m∈IμAμm†Aμm=1d.\sum_{\mu\in M} \sum_{m\in I_\mu} A_{\mu m}^\dagger A_{\mu m} = \mathbb 1_d .

Let ρμ′=∑mAμmρAμm†\rho'_\mu = \sum_m A_{\mu m}\rho A_{\mu m}^\dagger and pμ=tr⁡ρμ′p_\mu = \operatorname{tr}\rho'_\mu. Then

  1. every pμp_\mu is a nonnegative real number, and
  2. ∑μ∈Mpμ=1\sum_{\mu\in M} p_\mu = 1.

This is the statement in the source that "the trace of ρμ′\rho'_\mu is the probability of occurrence of outcome μ\mu", made precise.

Formalization Note Probabilities are complex numbers here; "pμ≥0p_\mu\ge 0" uses the standard partial order on C\mathbb C, meaning pμp_\mu is real and nonnegative.

Preamble
import Mathlib
import Definitions.Def_PeresTerno_kraus_basics

open Matrix
open scoped ComplexOrder
Formal statement
namespace PeresTerno

theorem outcome_probabilities_distribution {d e α : Type*} [Fintype d] [Fintype e] [Fintype α]
    {ι : α → Type*} [∀ μ, Fintype (ι μ)] [DecidableEq d]
    (A : ∀ μ, ι μ → Matrix e d ℂ) (hA : ∑ μ, povmElement (A μ) = 1)
    (ρ : Matrix d d ℂ) (hρ : IsDensityMatrix ρ) :
    (∀ μ, 0 ≤ trace (krausUpdate (A μ) ρ)) ∧ ∑ μ, trace (krausUpdate (A μ) ρ) = 1 := 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, text after Eq. (6) and Eqs. (7)-(8)
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.

Fix finite index types dd, ee and MM, and for each μ∈M\mu\in M a finite index type IμI_\mu. Let AμmA_{\mu m} (μ∈M\mu\in M, m∈Iμm\in I_\mu) be complex e×de\times d matrices satisfying

∑μ∈M∑m∈IμAμm†Aμm=1d,\sum_{\mu\in M}\sum_{m\in I_\mu} A_{\mu m}^\dagger A_{\mu m} = \mathbb 1_d ,

and let ρ\rho be a d×dd\times d density matrix (positive semidefinite, tr⁡ρ=1\operatorname{tr}\rho = 1). Then both:

  1. for every μ∈M\mu\in M, the complex number tr⁡(∑m∈IμAμmρAμm†)\operatorname{tr}\big(\sum_{m\in I_\mu} A_{\mu m}\rho A_{\mu m}^\dagger\big) is ≥0\ge 0 in the partial order of C\mathbb C (real part ≥0\ge 0 and imaginary part =0=0);
  2. ∑μ∈Mtr⁡(∑m∈IμAμmρAμm†)=1\sum_{\mu\in M} \operatorname{tr}\big(\sum_{m\in I_\mu} A_{\mu m}\rho A_{\mu m}^\dagger\big) = 1.

Edge cases: if dd is empty no density matrix exists and the statement is vacuous; if dd is nonempty, the completeness hypothesis forces MM to be nonempty. No condition is placed on ee beyond finiteness.

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