EPR geometric loss probabilities and sector overlaps

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.epr_loss_coefficients

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$ .

For one signal-idler pair and per-pair signal energy $N\ge0$ , the normalized NDS state is

|\psi_N\rangle=\sqrt{\frac1{N+1}}\sum_{n=0}^\infty\left(\sqrt{\frac N{N+1}}\right)^n|n\rangle_I|n\rangle_S.

Its mean signal energy is $N$ . The actual loss probability and overlap, with convergent defining series, satisfy

p_k^{(b)}=\frac{(T_bN)^k}{(T_bN+1)^{k+1}},\qquad I_k=\frac{(t_0t_1N)^k}{[(1-r_0r_1)N+1]^{k+1}},\quad T_b=1-R_b.

The integer powers give $p_0^{(b)}=I_0=1$ at $N=0$ and all positive-loss sectors vanish. This is the sector data for the EPR fidelity and Chernoff formulas.

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

/-- EPR geometric loss probabilities and loss-sector overlap, PDF p.9, (73)–(75).
N is per-pair signal energy, not total energy of a multipair probe. -/
theorem epr_loss_coefficients (c : Channels) (hc : ValidSplitters c) (hr : Reading c)
    (N : ℝ) (hN : 0 ≤ N) :
    Memℓp (tmsvCoefficients 1 N) 2 ∧ ‖tmsvProbe 1 N‖=1 ∧
    HasSignalEnergy (tmsvProbe 1 N) N ∧ IsNDS (tmsvProbe 1 N) ∧
    (∀ b k, lossProbability c (tmsvProbe 1 N) b (fun _ => k)=
      (((1-(c b).reflectance)*N)^k / ((1-(c b).reflectance)*N+1)^(k+1))) ∧
    (∀ k, Summable (lossOverlapTerm c (tmsvProbe 1 N) (fun _ => k)) ∧
      lossOverlap c (tmsvProbe 1 N) (fun _ => k)=
        (((c false).t*(c true).t*N)^k / ((1-(c false).r*(c true).r)*N+1)^(k+1) : ℝ)) := 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. 9, epr-loss-coefficients

Read-back

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

Let $c$ consist of splitters indexed by $b=0,1$ , with reflectances $R_b\in[0,1]$ and phases $\phi_b\in\mathbb R$ , satisfying $R_0\le R_1$ , $\sqrt{R_0}e^{i\phi_0}\ne\sqrt{R_1}e^{i\phi_1}$ , and $\phi_0=\phi_1=0$ , and let $N\in\mathbb R$ satisfy $N\ge0$ . Write $r_b=\sqrt{R_b}$ and $t_b=\sqrt{1-R_b}$ , and identify each one-mode occupation function with its unique natural-number value. Define $f:\mathbb N\times\mathbb N\to\mathbb C$ by

f(i,n)= \begin{cases} \displaystyle\sqrt{\frac1{N+1}} \left(\sqrt{\frac N{N+1}}\right)^n,&i=n,\\ 0,&i\ne n, \end{cases}

and let $\psi\in\ell^2(\mathbb N\times\mathbb N;\mathbb C)$ be this coefficient function if it is square summable, and the zero vector otherwise. For $n,k\in\mathbb N$ , define $a_b(n,k)=\sqrt{\binom nk}\,r_b^{n-k}t_b^k$ if $k\le n$ , and $0$ otherwise. Let $s_{b,k}$ be the coefficient function $(i,q)\mapsto\psi(i,q+k)a_b(q+k,k)$ as an $\ell^2$ vector if square summable, and $0$ otherwise, and put $p_n=\sum_i|\psi(i,n)|^2$ . The assertion is that $f$ is square summable, $\|\psi\|=1$ , $n\mapsto np_n$ is summable with $\sum_nnp_n=N$ , and

\sum_i\psi(i,n)\overline{\psi(i,q)}=0 \quad\text{for all }n\ne q.

Furthermore, every $b\in\{0,1\}$ and $k\in\mathbb N$ satisfy

\|s_{b,k}\|^2 =\frac{\bigl((1-R_b)N\bigr)^k} {\bigl((1-R_b)N+1\bigr)^{k+1}},

and for every $k\in\mathbb N$ , the complex-valued family $n\mapsto p_n\overline{a_0(n,k)}a_1(n,k)$ is summable and

\langle s_{0,k},s_{1,k}\rangle =\frac{(t_0t_1N)^k} {\bigl((1-r_0r_1)N+1\bigr)^{k+1}},

where the real number on the right is regarded as a complex number. The statement includes $N=0$ , $k=0$ , and reflectance endpoints; zeroth powers, including $0^0$ , equal $1$ , and all the displayed denominators are positive under the hypotheses. Infinite sums use the total-sum convention, giving $0$ for a nonsummable family, although summability is explicitly asserted for the moment and overlap families above.

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