Prove2Me

Expected fidelity F(ψ,ρ)=⟨ψ∣ρ∣ψ⟩F(\psi,\rho) = \langle\psi|\rho|\psi\rangle

Definition
WildeQIT_expectedFidelity

by aadarwal · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

density-operatorfidelitymatrix-analysisquantum-informationwilde-qit

Definition 9.2.2 (Expected Fidelity). The expected fidelity F(ψ,ρ)F(\psi, \rho) between a pure state ∣ψ⟩∈H|\psi\rangle \in \mathcal{H} and a mixed state ρ∈D(H)\rho \in \mathcal{D}(\mathcal{H}) is

F(ψ,ρ)≡⟨ψ∣ρ∣ψ⟩.F(\psi, \rho) \equiv \langle \psi | \rho | \psi \rangle .

It is the probability that ρ\rho passes the test {∣ψ⟩⟨ψ∣,I−∣ψ⟩⟨ψ∣}\{|\psi\rangle\langle\psi|, I - |\psi\rangle\langle\psi|\} (Exercise 9.2.2) and the expected pure-state fidelity over any ensemble decomposition of ρ\rho.

Formalization Note. WildeQIT.expectedFidelity ψ ρ = (star ψ ⬝ᵥ (ρ *ᵥ ψ)).re, the real part of ⟨ψ∣ρ∣ψ⟩\langle\psi|\rho|\psi\rangle (which is real when ρ\rho is Hermitian); ψ : n → ℂ, ρ : Matrix n n ℂ.

Definition code
import Mathlib.LinearAlgebra.Matrix.DotProduct
import Mathlib.Data.Matrix.Mul
import Mathlib.Analysis.Complex.Basic

/-!
Wilde, *Quantum Information Theory* (2nd ed.), §9.2.2, Definition 9.2.2 (Expected Fidelity).

The expected fidelity `F(ψ, ρ)` between a pure state `|ψ⟩ ∈ ℋ` and a mixed state `ρ ∈ 𝒟(ℋ)` is
`F(ψ, ρ) ≡ ⟨ψ|ρ|ψ⟩`.
-/

open Matrix

namespace WildeQIT

/-- **Definition 9.2.2 (Expected Fidelity).** For a vector `ψ : n → ℂ` and a matrix
`ρ : Matrix n n ℂ`, `expectedFidelity ψ ρ = ⟨ψ|ρ|ψ⟩`, recorded as the real part of the complex
number `star ψ ⬝ᵥ (ρ *ᵥ ψ)` (which is real when `ρ` is Hermitian). -/
noncomputable def expectedFidelity {n : Type} [Fintype n] (ψ : n → ℂ) (ρ : Matrix n n ℂ) : ℝ :=
  (star ψ ⬝ᵥ (ρ *ᵥ ψ)).re

end WildeQIT
Source
Wilde, *Quantum Information Theory*, 2nd ed. (Cambridge University Press, 2017; arXiv:1106.1445v8), §9.2.2 "Expected Fidelity", Definition 9.2.2 (Expected Fidelity).

View graph