Uhlmann fidelity — the core

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

The fidelity of two states,

F(ρ, σ) = Tr √(√ρ · σ · √ρ) = ∑ᵢ √(λᵢ(√ρ σ √ρ)),

defined spectrally, exactly as traceNorm is (TraceDistance.lean). The sandwich √ρ σ √ρ is positive semidefinite (posSemidef_sandwich), so every eigenvalue is nonnegative and the square roots are real.

What this module delivers:

• the definition, and non-negativity (fidelity_nonneg);
• ★ symmetry F(ρ, σ) = F(σ, ρ) (fidelity_comm) — the one property that is normally real work, because the two sandwiches √ρ σ √ρ and √σ ρ √σ are different matrices. It falls out of the corpus's own rectangular-spectrum lemma spectral_sum_mul_conjTranspose_comm (∑ g(λ(M Mᴴ)) = ∑ g(λ(Mᴴ M)) for g 0 = 0) at M = √σ √ρ, since Mᴴ M = √ρ σ √ρ and M Mᴴ = √σ ρ √σ;
• the transport hinge sqrt_eigenvalue_sum_congr (eigenvalue sums depend on the matrix, not on the supplied Hermitian witness), which is what lets the two sandwiches be compared at all.

★ The upper bound is proved (2026-09-01): fidelity_le_one, for states that are positive definite. The route builds the two missing pieces rather than importing them — Hilbert–Schmidt Cauchy–Schwarz (norm_trace_conjTranspose_mul_le, by transporting matrices to EuclideanSpace ℂ (n × n), since Mathlib gives Matrix only a Frobenius norm and no inner product) and the polar decomposition of an invertible matrix (exists_unitary_conjTranspose_mul_eq_sqrt, elementary: U = X P⁻¹).

Honest scope. Positive-definiteness in fidelity_le_one is load-bearing, not decorative: it makes X = √σ √ρ invertible, and the elementary polar decomposition exists only for invertible X. Removing it needs a general polar/singular-value factorisation, which Mathlib does not have — it has singular values (LinearMap.singularValues) but no A = U Σ Vᴴ. MATHLIB-ABSENT(Matrix.polarDecomposition) This is the same posture as klein_inequality, which carries a PosDef hypothesis for a related reason. F = 1 ↔ ρ = σ, monotonicity under channels, Uhlmann's theorem and Fuchs–van de Graaf are not attempted. The purification half Uhlmann also needs is in the corpus (QuantumInfo.exists_purification, Subadditivity.lean).

Reference: Nielsen–Chuang §9.2.2 (fidelity); Uhlmann, Rep. Math. Phys. 9 (1976) 273. In-corpus: Mathlib/QuantumInfo/TraceDistance.lean (the sibling metric), Mathlib/QuantumInfo/Subadditivity.lean (sqrtMat, the spectrum lemma, purification).

theorem QuantumInfo.posSemidef_sandwich {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) : (sqrtMat ⋯ * σ * sqrtMat ⋯).PosSemidef

The sandwich √ρ · σ · √ρ is positive semidefinite: it is Bᴴ σ B at B = √ρ, which is Hermitian.

noncomputable def QuantumInfo.fidelity {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) : ℝ

Uhlmann fidelity F(ρ, σ) = Tr √(√ρ σ √ρ), defined spectrally as the sum of the square roots of the (nonnegative) eigenvalues of the sandwich.

Equations

• QuantumInfo.fidelity hρ hσ = ∑ i : n, √(⋯.eigenvalues i)

theorem QuantumInfo.sqrt_eigenvalue_sum_congr {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (h : A = B) : ∑ i : n, √(hA.eigenvalues i) = ∑ i : n, √(hB.eigenvalues i)

Transport of a √-eigenvalue sum along an equality of matrices: the eigenvalues are determined by the matrix, not by the supplied Hermitian witness. Same proof-irrelevance hinge as entropy_congr_of_eq.

theorem QuantumInfo.fidelity_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) : 0 ≤ fidelity hρ hσ

Fidelity is nonnegative.

theorem QuantumInfo.fidelity_comm {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) : fidelity hρ hσ = fidelity hσ hρ

★ Fidelity is symmetric, F(ρ, σ) = F(σ, ρ), even though the two sandwiches √ρ σ √ρ and √σ ρ √σ are different matrices. At M = √σ √ρ one has Mᴴ M = √ρ σ √ρ and M Mᴴ = √σ ρ √σ, so this is spectral_sum_mul_conjTranspose_comm with g = √ (and √0 = 0).

The Hilbert–Schmidt Cauchy–Schwarz inequality

Mathlib has no inner-product structure on Matrix (only the Frobenius norm), so the inequality is obtained by transporting matrices to EuclideanSpace ℂ (n × n), where norm_inner_le_norm is Cauchy–Schwarz.

noncomputable def QuantumInfo.vecOf {n : Type u_1} (A : Matrix n n ℂ) : EuclideanSpace ℂ (n × n)

A matrix read as a vector of ℂ^{n×n}.

Equations

• QuantumInfo.vecOf A = WithLp.toLp 2 fun (p : n × n) => A p.1 p.2

theorem QuantumInfo.inner_vecOf {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : inner ℂ (vecOf A) (vecOf B) = (A.conjTranspose * B).trace

theorem QuantumInfo.norm_sq_vecOf {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : ‖vecOf A‖ ^ 2 = (A.conjTranspose * A).trace.re

theorem QuantumInfo.norm_trace_conjTranspose_mul_le {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : ‖(A.conjTranspose * B).trace‖ ≤ √(A.conjTranspose * A).trace.re * √(B.conjTranspose * B).trace.re

★ Hilbert–Schmidt Cauchy–Schwarz: |Tr(Aᴴ B)| ≤ ‖A‖₂ ‖B‖₂.

Polar decomposition for an invertible matrix

Mathlib has singular values (LinearMap.singularValues) but no A = U Σ Vᴴ and no polar factorisation. MATHLIB-ABSENT(Matrix.polarDecomposition) For an invertible X the construction is elementary: P := √(Xᴴ X) is positive definite, hence invertible, and U := X P⁻¹ is unitary. That is all the fidelity bound needs, and it is why fidelity_le_one below carries positive-definiteness hypotheses.

theorem QuantumInfo.exists_unitary_conjTranspose_mul_eq_sqrt {n : Type u_1} [Fintype n] [DecidableEq n] {X : Matrix n n ℂ} (hXX : (X.conjTranspose * X).PosDef) : ∃ U ∈ Matrix.unitaryGroup n ℂ, U.conjTranspose * X = sqrtMat ⋯

For invertible X, the unitary factor of the polar decomposition, characterised by the identity the fidelity bound consumes: Uᴴ X = √(Xᴴ X). Invertibility of P = √(Xᴴ X) comes from det P * det P = det (Xᴴ X), so no separate positive-definiteness argument is needed.

★★ The upper bound

theorem QuantumInfo.sqrtMat_isUnit {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.PosDef) : IsUnit (sqrtMat ⋯)

√ρ is invertible when ρ is positive definite (det √ρ * det √ρ = det ρ ≠ 0).

theorem QuantumInfo.posDef_sandwich {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosDef) (hσ : σ.PosDef) : (sqrtMat ⋯ * σ * sqrtMat ⋯).PosDef

The sandwich √ρ σ √ρ is positive definite when both states are.

theorem QuantumInfo.fidelity_eq_re_trace {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) : fidelity hρ hσ = RCLike.re (sqrtMat ⋯).trace

Fidelity as the trace of the matrix square root of the sandwich.

theorem QuantumInfo.sqrtMat_trace_congr {n : Type u_1} [Fintype n] [DecidableEq n] {M N : Matrix n n ℂ} (hM : M.IsHermitian) (hN : N.IsHermitian) (h : M = N) : RCLike.re (sqrtMat hM).trace = RCLike.re (sqrtMat hN).trace

Transport of Tr √· along an equality of matrices — the same proof-irrelevance hinge as sqrt_eigenvalue_sum_congr.

theorem QuantumInfo.fidelity_le_one {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (hρ : ρ.PosDef) (hσ : σ.PosDef) (hρ1 : ρ.trace = 1) (hσ1 : σ.trace = 1) : fidelity ⋯ ⋯ ≤ 1

★★ F(ρ,σ) ≤ 1 for states. The route: Xᴴ X = √ρ σ √ρ at X = √σ √ρ, so the polar factor of X has trace F; writing that trace as a Hilbert–Schmidt inner product ⟪√σ U, √ρ⟫ and applying Cauchy–Schwarz gives F ≤ ‖√σ U‖₂ ‖√ρ‖₂ = √(Tr σ) √(Tr ρ) = 1.

⚠️ Positive-definiteness is load-bearing, not decorative: it is what makes X invertible, and the elementary polar decomposition used here (U = X P⁻¹) exists only for invertible X. Mathlib has no general polar/singular-value factorisation to remove the hypothesis with.