Multipair EPR fidelity and lower error bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.epr_fidelity

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

prove2quantum

Let $M\ge1$ be the finite number of signal modes and $J\ge0$ the finite number of retained idler modes, on the full optical Fock spaces. The two channels have equal priors, independent vacuum environments, reflectances $0\le R_0\le R_1\le1$ , field magnitudes $r_b=\sqrt{R_b}$ and $t_b=\sqrt{1-R_b}$ , and distinct complex reflection coefficients $r_b e^{i\theta_b}$ . Every signal mode sees the same channel; idlers are retained losslessly and environment outputs are inaccessible. Write $\mathcal F$ for squared Uhlmann fidelity, $P_e$ for minimum average error over all joint binary receivers, $Q_s=\operatorname{Tr}(\rho_0^s\rho_1^{1-s})$ , and $Q=\min_{0\le s\le1}Q_s$ , with zero powers interpreted as support projections. Here the common phase is removed, so $\theta_0=\theta_1=0$ and $R_0<R_1$ . Put $\mu=r_0r_1+t_0t_1$ .

Let $M\ge1$ identical EPR pairs each have signal energy $N\ge0$ . Their product is normalized and has total mean signal energy $N_s=MN$ . Then

\mathcal F=[1+(1-\mu)N]^{-2M},\qquad P_e\ge\frac{1-\sqrt{1-[1+(1-\mu)N]^{-2M}}}{2}.

The one-pair case is equation (76). The error expression is a lower bound, with its factor $1/2$ , and is not an exact error formula for EPR probes.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P54

Formal statement

noncomputable section

open scoped BigOperators ComplexConjugate

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P54

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Claimed50.P47 (Occupation)

open QAlgorithms.Papers.Independent.Dependency50.P39 (coherentCoefficient)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- Multipair EPR fidelity and LOWER error bound, PDF pp.9–10, (76),(87),(91).
The prior factor 1/2 is included in lowerError; this is not an exact EPR opticalError formula. -/
theorem epr_fidelity (M : ℕ) (hM : 0 < M) (c : Channels) (hc : ValidSplitters c)
    (hr : Reading c) (N : ℝ) (hN : 0 ≤ N) :
    Memℓp (tmsvCoefficients M N) 2 ∧ ‖tmsvProbe M N‖=1 ∧
    HasSignalEnergy (tmsvProbe M N) ((M : ℝ)*N) ∧
    outputFidelity c (tmsvProbe M N)=((1-splitterOverlap c)*N+1)^(-(2*M : ℤ)) ∧
    lowerError (((1-splitterOverlap c)*N+1)^(-(2*M : ℤ))) ≤ outputError c (tmsvProbe M N) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P54

end

Source

Discriminating quantum-optical beam-splitter channels with number-diagonal signal states: Applications to quantum reading and target detection, arXiv:1105.4063v3, PDF p. 10, epr-fidelity

Read-back

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

Let $M$ be a positive natural number, and let $c$ specify two splitters, indexed by $b\in\{0,1\}$ , with reflectances $R_b\in[0,1]$ and phases $\theta_b\in\mathbb R$ . Assume $R_0\le R_1$ , $\sqrt{R_0}e^{i\theta_0}\ne\sqrt{R_1}e^{i\theta_1}$ , and $\theta_0=\theta_1=0$ ; in particular, $R_0<R_1$ . Put $r_b=\sqrt{R_b}$ , $t_b=\sqrt{1-R_b}$ , and $\mu=r_0r_1+t_0t_1$ . Let $N\ge0$ . An occupation vector is $n\in\mathbb N^M$ , with total occupation $|n|=\sum_m n_m$ , and the Hilbert spaces below are complex square-summable functions on their indicated index sets. Define

a_{M,N}(p,n)= \begin{cases} \displaystyle\prod_{m=1}^{M}\sqrt{\frac1{N+1}} \left(\sqrt{\frac N{N+1}}\right)^{n_m},&p=n,\\ 0,&p\ne n. \end{cases}

The probe $\psi_{M,N}$ is this coefficient function regarded as a square-summable vector if it is square-summable, and is the zero vector otherwise. For any probe $\psi$ on $\mathbb N^M\times\mathbb N^M$ , define

A_b(n,k)= \begin{cases} \displaystyle\prod_m\sqrt{\binom{n_m}{k_m}}\, r_b^{\,n_m-k_m}t_b^{\,k_m},&k_m\le n_m\text{ for every }m,\\ 0,&\text{otherwise}, \end{cases} \qquad K_b^\psi((p,n),(q,v)) =\sum_{k\in\mathbb N^M} \psi(p,n+k)A_b(n+k,k)\, \overline{\psi(q,v+k)A_b(v+k,k)}.

For kernels $K,L$ on an index set $X$ , define $F(K,L)$ as the real supremum of $|\langle z,w\rangle|^2$ over unit vectors $z,w\in\ell^2(X\times\mathbb N;\mathbb C)$ satisfying $K(x,y)=\sum_e z(x,e)\overline{z(y,e)}$ and $L(x,y)=\sum_e w(x,e)\overline{w(y,e)}$ . A resolution of $K$ consists of nonnegative summable weights $a_j$ with $\sum_j a_j=1$ , vectors $u_j\in\ell^2(X;\mathbb C)$ that have norm one whenever $a_j>0$ , are mutually orthogonal whenever their distinct indices have positive weights, and satisfy $K(x,y)=\sum_j a_j u_j(x)\overline{u_j(y)}$ ; vectors with zero weight need not be normalized. Define $P(K,L)$ as the real infimum, over resolutions $(a_j,u_j)$ , $(b_j,v_j)$ of $K,L$ and bounded complex-linear operators $E$ satisfying $E=E^*$ and $0\le\langle v,Ev\rangle_{\mathbb R}\le\|v\|^2$ for every $v$ , of

\frac12\sum_j a_j\bigl(1-\operatorname{Re}\langle u_j,Eu_j\rangle\bigr) +\frac12\sum_j b_j\operatorname{Re}\langle v_j,Ev_j\rangle.

These are the specified real supremum and infimum constructions, with value zero for an empty defining set. The declaration asserts that $a_{M,N}$ is square-summable, $\|\psi_{M,N}\|=1$ , and, writing $p_\psi(n)=\sum_p|\psi(p,n)|^2$ and $q_\psi(j)=\sum_{|n|=j}p_\psi(n)$ , the real series $\sum_{j\ge0}j q_{\psi_{M,N}}(j)$ is summable and has sum $MN$ , which is nonnegative. It also asserts

F(K_0^{\psi_{M,N}},K_1^{\psi_{M,N}}) =\bigl((1-\mu)N+1\bigr)^{-2M}, \qquad \frac{1-\sqrt{\,1-\bigl((1-\mu)N+1\bigr)^{-2M}}}{2} \le P(K_0^{\psi_{M,N}},K_1^{\psi_{M,N}}).

The exponents here are integer powers. The case $N=0$ is included, with zeroth powers interpreted as one.

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