General pure-probe fidelity and error lower bounds

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.general_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.

Let $\lvert\psi\rangle$ be any normalized pure joint probe, with total signal photon law $p_n$ , and set $\Delta=\theta_1-\theta_0$ and $\mu=r_0r_1+t_0t_1$ . Its loss-sector amplitudes are square summable, $\sum_n p_n=1$ , and the following complex series is absolutely convergent:

O(\psi)=\left|\sum_{n=0}^\infty p_n e^{in\Delta}\mu^n\right|^2\le\mathcal F(\psi),\qquad \frac{1-\sqrt{1-O(\psi)}}2\le P_e(\psi).

This lower bound applies without a finite-energy assumption or any restriction on idler correlations.

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

/-- General fidelity bound and its operational error consequence, PDF pp.3–4,
(11)–(20). No finite-energy or signal-idler orthogonality hypothesis is imposed. -/
theorem general_fidelity {M J : ℕ} (hM : 0 < M) (c : Channels) (hc : ValidSplitters c)
    (psi : Hilbert (Occupation (Fin J) × Occupation (Fin M))) (hpsi : ‖psi‖ = 1) :
    (∀ b k, Memℓp (sectorCoefficients (c b) psi k) 2) ∧
    Summable (totalLaw psi) ∧ (∑' n, totalLaw psi n) = 1 ∧
    Summable (purificationOverlapTerm c psi) ∧
    purificationOverlap c psi ≤ outputFidelity c psi ∧
    lowerError (purificationOverlap c psi) ≤ outputError c psi := 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. 1, general-fidelity

Read-back

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

Let $M,J\in\mathbb N$ with $M>0$ , allowing $J=0$ . For $b\in\{0,1\}$ , let the splitter $c_b$ have reflectance $R_b\in[0,1]$ , phase $\theta_b\in\mathbb R$ , $r_b=\sqrt{R_b}$ , and $t_b=\sqrt{1-R_b}$ ; assume $R_0\le R_1$ and $r_0e^{i\theta_0}\ne r_1e^{i\theta_1}$ . Let $\psi\in\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ have norm $1$ . For signal occupations $n,k\in\mathbb N^M$ , define

L_b(n,k)= \begin{cases} \displaystyle\prod_{m=0}^{M-1} \sqrt{\binom{n_m}{k_m}}\,e^{in_m\theta_b} r_b^{\,n_m-k_m}t_b^{\,k_m},&k_m\le n_m\text{ for every }m,\\ 0,&\text{otherwise}, \end{cases}

and $g_{b,k}(i,p)=\psi(i,p+k)L_b(p+k,k)$ . Define the returned kernels $\rho_b(x,y)=\sum_k g_{b,k}(x)\overline{g_{b,k}(y)}$ , the occupation weights $p_n=\sum_{i\in\mathbb N^J}|\psi(i,n)|^2$ , the total-number weights $P_N=\sum_{n:\,\sum_m n_m=N}p_n$ , the splitter overlap $o=r_0r_1+t_0t_1$ , and $z_N=P_Ne^{iN(\theta_1-\theta_0)}o^N$ . Write $U=\left|\sum_Nz_N\right|^2$ . Here the output fidelity $F$ is the real supremum of $|\langle z,w\rangle|^2$ over unit vectors $z,w\in\ell^2((\mathbb N^J\times\mathbb N^M)\times\mathbb N;\mathbb C)$ satisfying $\sum_e z(x,e)\overline{z(y,e)}=\rho_0(x,y)$ and $\sum_e w(x,e)\overline{w(y,e)}=\rho_1(x,y)$ . The output error $E$ is the real infimum of

\frac12\sum_n a_n\bigl(1-\operatorname{Re}\langle u_n,Tu_n\rangle\bigr) +\frac12\sum_n b_n\operatorname{Re}\langle v_n,Tv_n\rangle

over resolutions $\rho_0(x,y)=\sum_n a_nu_n(x)\overline{u_n(y)}$ and $\rho_1(x,y)=\sum_n b_nv_n(x)\overline{v_n(y)}$ , and bounded complex-linear operators $T$ satisfying $\langle u,Tv\rangle=\overline{\langle v,Tu\rangle}$ and $0\le\operatorname{Re}\langle v,Tv\rangle\le\|v\|^2$ for all vectors. Each resolution has summable nonnegative weights of total mass $1$ , unit vectors at positive weights, and orthogonal vectors at distinct positive weights; zero-weight vectors are unrestricted. Empty defining sets for these real suprema or infima give value $0$ . The theorem asserts that every $g_{b,k}$ is square-summable, that $(P_N)_{N\in\mathbb N}$ is summable with sum $1$ , that $(z_N)_{N\in\mathbb N}$ is summable, and that

U\le F,\qquad \frac{1-\sqrt{1-U}}2\le E.

Zero occupations and endpoint reflectances are included; occupation-vector subtraction in $L_b$ is natural-number subtraction, and natural powers use $0^0=1$ .

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