Prove2Me

Section 3.3: purification and equality of complementary entropies

Open
QAlgorithms.Papers.Independent.Intakethird100.P51.purification

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Every finite normalized positive semidefinite state ρA\rho_A has a finite nonzero auxiliary system BB and a unit vector ψAB\psi_{AB} such that

Tr⁡B∣ψ⟩⟨ψ∣=ρA,S(ρB)=S(ρA).\operatorname{Tr}_B|\psi\rangle\langle\psi|=\rho_A,\qquad S(\rho_B)=S(\rho_A).

Moreover, for every bipartite unit vector, its two reduced states have equal entropy. Singular states are permitted. The existence of the purification is part of the conclusion and supplies the complementary-entropy method.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P51
Formal statement
noncomputable section

open scoped Matrix ComplexOrder ComplexConjugate Matrix.Norms.L2Operator

open MeasureTheory

namespace QAlgorithms.Papers.Independent.Intakethird100.P51

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact interfaces from the frozen accepted library; no local redeclarations.

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Information100.P56 (entropy holevo IsLaw)

open QAlgorithms.Papers.Independent.Information100.P27 (average)

open QAlgorithms.Papers.Independent.Dependency50.P21 (relativeEntropy marginalAB channelAdjoint)

open QAlgorithms.Papers.Independent.Dependency50.P35 (marginalAC)

open QAlgorithms.Papers.Independent.Gap48.P19 (shannonNats)

open QAlgorithms.Papers.Independent.Gap48.P33 (measurementInformation)

section Statements

variable {A B C D J K O : Type}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D] [Fintype J] [Fintype K] [Fintype O]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

variable [DecidableEq J] [DecidableEq K] [DecidableEq O]

/-- Section 3.3, PDF p.9: purification exists; complementary entropies agree for
all unit bipartite pure states, including singular density matrices. -/
theorem purification [Nonempty A] [Nonempty B] (rho : Mat A) (h : IsDensityMatrix rho) :
    (∃ m : ℕ, 0 < m ∧ ∃ psi : EuclideanSpace ℂ (A × Fin m),
      ‖psi‖ = 1 ∧ traceRight (pureDensity psi) = rho ∧
        entropy (traceLeft (pureDensity psi)) = entropy rho) ∧
    (∀ psi : EuclideanSpace ℂ (A × B), ‖psi‖ = 1 →
      entropy (traceRight (pureDensity psi)) = entropy (traceLeft (pureDensity psi))) := by sorry

end Statements

end QAlgorithms.Papers.Independent.Intakethird100.P51

end
Source
Inequalities for Quantum Entropy: A Review with Conditions for Equality, arXiv:quant-ph/0205064v2, PDF p. 9, Section 3.3: purification and equality of complementary entropies
Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For finite nonempty index types A,BA,B with decidable equality and every positive semidefinite complex matrix ρ\rho on AA with trace 11, there exist a natural number m>0m>0 and a vector ψ∈CA×{0,…,m−1}\psi\in\mathbb C^{A\times\{0,\ldots,m-1\}} of Euclidean norm 11 such that Tr⁡{0,…,m−1}∣ψ⟩⟨ψ∣=ρ\operatorname{Tr}_{\{0,\ldots,m-1\}}|\psi\rangle\langle\psi|=\rho and S(Tr⁡A∣ψ⟩⟨ψ∣)=S(ρ)S(\operatorname{Tr}_A|\psi\rangle\langle\psi|)=S(\rho). In addition, every vector ψ∈CA×B\psi\in\mathbb C^{A\times B} of Euclidean norm 11 satisfies S(Tr⁡B∣ψ⟩⟨ψ∣)=S(Tr⁡A∣ψ⟩⟨ψ∣)S(\operatorname{Tr}_B|\psi\rangle\langle\psi|)=S(\operatorname{Tr}_A|\psi\rangle\langle\psi|). Here ∣ψ⟩⟨ψ∣|\psi\rangle\langle\psi| has entries ψiψj‾\psi_i\overline{\psi_j}, partial traces sum over the discarded index, and S(M)=−Re⁡tr⁡(f(M))S(M)=-\operatorname{Re}\operatorname{tr}(f(M)), with f(x)=xlog⁡xf(x)=x\log x applied by continuous functional calculus using natural logarithms and log⁡0=0\log0=0. Singular density matrices and registers of cardinality 11 are included.

Human review

  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph