Pure-state fidelity $F(\psi,\phi) = |\langle\psi|\phi\rangle|^2$

Definition

WildeQIT_pureFidelity

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

density-operatorfidelitymatrix-analysisquantum-informationwilde-qit

Definition 9.2.1 (Pure-State Fidelity). Let $|\psi\rangle, |\phi\rangle \in \mathcal{H}$ be pure states. The pure-state fidelity is the squared overlap of the states:

F(\psi, \phi) \equiv |\langle \psi | \phi \rangle|^2 .

It is the probability that a state prepared as $|\phi\rangle$ passes the test "is it $|\psi\rangle$ ?", and is the special case of the general fidelity (Uhlmann's theorem, Exercise 9.2.5) for two pure states.

Formalization Note. Vectors are ψ φ : n → ℂ on a finite index type; WildeQIT.pureFidelity ψ φ = ‖star ψ ⬝ᵥ φ‖ ^ 2 with $\langle\psi|\phi\rangle = \sum_i \overline{\psi_i}\phi_i$ . Normalization is not part of the definition; theorems add it as a hypothesis.

Definition code

import Mathlib.LinearAlgebra.Matrix.DotProduct
import Mathlib.Analysis.Complex.Basic

/-!
Wilde, *Quantum Information Theory* (2nd ed.), §9.2.1, Definition 9.2.1 (Pure-State Fidelity).

Let `|ψ⟩, |φ⟩ ∈ ℋ` be pure states. The pure-state fidelity is the squared overlap
`F(ψ, φ) ≡ |⟨ψ|φ⟩|²`.
-/

open Matrix

namespace WildeQIT

/-- **Definition 9.2.1 (Pure-State Fidelity).** For vectors `ψ φ : n → ℂ`,
`pureFidelity ψ φ = |⟨ψ|φ⟩|²` where `⟨ψ|φ⟩ = ∑ᵢ conj(ψᵢ) φᵢ`. -/
noncomputable def pureFidelity {n : Type} [Fintype n] (ψ φ : n → ℂ) : ℝ :=
  ‖star ψ ⬝ᵥ φ‖ ^ 2

end WildeQIT

Source

Wilde, *Quantum Information Theory*, 2nd ed. (Cambridge University Press, 2017; arXiv:1106.1445v8), §9.2.1 "Pure-State Fidelity", Definition 9.2.1 (Pure-State Fidelity).

View graph

Pure-state fidelity F(ψ,ϕ)=∣⟨ψ∣ϕ⟩∣2F(\psi,\phi) = |\langle\psi|\phi\rangle|^2F(ψ,ϕ)=∣⟨ψ∣ϕ⟩∣2

Pure-state fidelity $F(\psi,\phi) = |\langle\psi|\phi\rangle|^2$