Observable distortion equals one minus source entanglement fidelity

Open

QAlgorithms.Papers.Independent.Intakethird100.P27.observable_entanglement_fidelity

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

prove2quantum

Let $A$ be a finite nonempty register, let $\psi_{RA}$ be a unit vector with $R$ isomorphic to $A$ , and let $\mathcal N:A\to A$ be CPTP. Write $P=|\psi\rangle\langle\psi|$ , $\omega=(\mathrm{id}_R\otimes\mathcal N)(P)$ , and $F_e=\langle\psi|\omega|\psi\rangle$ . Then $I-P$ is positive semidefinite and

\operatorname{Tr}[(I-P)\omega]=1-F_e.

Thus the general positive-observable distortion model includes the original entanglement-fidelity distortion for any source density, including rank-deficient sources.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P27

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P27

open Filter

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P19
  (first marginalRB mutualInformation bipartiteBlock epr)

open QAlgorithms.Papers.Independent.Information100.P08 (formation)

open QAlgorithms.Papers.Independent.Gap48.P20 (redistributionMarginal)

open QAlgorithms.Papers.Independent.Bridge50.P37 (isotropicState normalizedEntangledProjection)

/-- PDF p.5, Example 6: I-|psi><psi| is a positive observable and its expected
distortion is exactly one minus the general source entanglement fidelity. -/
theorem observable_entanglement_fidelity {A : Type} [Fintype A] [Nonempty A]
    (v : EuclideanSpace ℂ (A × A)) (hv : ‖v‖ = 1)
    (N : Superop A A) (hN : IsChannel N) :
    (1 - pureDensity v).PosSemidef ∧
      effectProb (1 - pureDensity v) (idTensorSuperop N (pureDensity v)) =
        1 - sourceFidelity v N := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P27

end

Source

Quantum rate distortion coding with auxiliary resources, arXiv:1212.5316v3, PDF p. 5, Example 6

Read-back

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

For every finite nonempty type $A$ , every $v\in\mathbb C^{A\times A}$ with $\|v\|=1$ , and every matrix function $N$ admitting a finite Kraus representation

N(X)=\sum_jK_jXK_j^\dagger,\qquad \sum_jK_j^\dagger K_j=I_A,

let $P=vv^\dagger$ , meaning $P(i,j)=v(i)\overline{v(j)}$ , and define $Y$ by applying $N$ to each block of $P$ :

Y((r,a),(s,b)) =N\bigl((v(r,x)\overline{v(s,y)})_{x,y\in A}\bigr)(a,b).

Then $I_{A\times A}-P$ is positive semidefinite, and

\operatorname{Re}\operatorname{Tr}\bigl((I-P)Y\bigr) = 1-\operatorname{Re}\sum_{i,j\in A\times A}\overline{v(i)}\,Y(i,j)\,v(j).

The assertion includes the case where $A$ has one element.

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