EPR Chernoff coefficient and piecewise optimizer

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.epr_chernoff

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

Assume $R_1<1$ and $N>0$ . Put $T_b=1-R_b$ ,

\alpha=\frac{T_0N+1}{T_1N+1},\quad\beta=\frac{T_0}{T_1},\quad C=\frac{[(1-r_0r_1)N+1]^2}{T_0N+1},\quad D=T_1N.

Then $1<\alpha<\beta$ and $C>D>0$ . For every $s\in[0,1]$ , $C\alpha^s-D\beta^s>0$ and the $M$ -pair coefficient is

Q_s^{(1)}=(C\alpha^s-D\beta^s)^{-1},\qquad Q_s^{(M)}=(Q_s^{(1)})^M.

Write $d=D\ln\beta-C\ln\alpha$ . If $d\ge0$ choose $s_*=0$ ; otherwise choose

s_*=\min\left\{1,\frac{\ln[(C\ln\alpha)/(D\ln\beta)]}{\ln(\beta/\alpha)}\right\}.

This $s_*\in[0,1]$ attains $Q^{(M)}$ and $P_e\le\tfrac12(C\alpha^{s_*}-D\beta^{s_*})^{-M}$ . At $N=0$ the logarithmic optimizer is bypassed: $\mathcal F=Q=1$ and $P_e=1/2$ . The ideal-memory endpoint is treated separately.

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 Chernoff expression and computed optimizer, PDF pp.9–10, (77)–(88).
The derivative test uses D ln beta-C ln alpha. Ideal memory and N=0 never use
beta=T0/T1 or the logarithmic critical-point expression. -/
theorem epr_chernoff (M : ℕ) (hM : 0 < M) (c : Channels) (hc : ValidSplitters c)
    (hr : Reading c) (hloss : (c true).reflectance < 1) :
    (∀ N : ℝ, 0 < N →
      1 < eprAlpha c N ∧ eprAlpha c N < eprBeta c ∧
      0 < eprD c N ∧ eprD c N < eprC c N ∧
      (∀ s ∈ Set.Icc (0 : ℝ) 1,
        0 < eprC c N * Real.rpow (eprAlpha c N) s - eprD c N * Real.rpow (eprBeta c) s ∧
        outputChernoffAt c (tmsvProbe 1 N) s =
          (eprC c N * Real.rpow (eprAlpha c N) s - eprD c N * Real.rpow (eprBeta c) s)⁻¹ ∧
        outputChernoffAt c (tmsvProbe M N) s=(outputChernoffAt c (tmsvProbe 1 N) s)^M) ∧
      eprOptimizer c N ∈ Set.Icc (0 : ℝ) 1 ∧
      (∀ s ∈ Set.Icc (0 : ℝ) 1,
        outputChernoffAt c (tmsvProbe M N) (eprOptimizer c N) ≤ outputChernoffAt c (tmsvProbe M N) s) ∧
      outputChernoff c (tmsvProbe M N)=outputChernoffAt c (tmsvProbe M N) (eprOptimizer c N) ∧
      outputError c (tmsvProbe M N) ≤ (1/2) *
        (eprC c N * Real.rpow (eprAlpha c N) (eprOptimizer c N) -
          eprD c N * Real.rpow (eprBeta c) (eprOptimizer c N))^(-(M : ℤ))) ∧
    outputFidelity c (tmsvProbe M 0)=1 ∧ outputChernoff c (tmsvProbe M 0)=1 ∧
    outputError c (tmsvProbe M 0)=1/2 := 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-chernoff

Read-back

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

Let $M$ be a positive natural number and let two splitters have reflectances $R_b\in[0,1]$ and phases $\theta_b$ , for $b\in\{0,1\}$ , with $R_0\le R_1$ , $\sqrt{R_0}e^{i\theta_0}\ne\sqrt{R_1}e^{i\theta_1}$ , $\theta_0=\theta_1=0$ , and $R_1<1$ ; thus $0\le R_0<R_1<1$ , allowing $R_0=0$ . Put $r_b=\sqrt{R_b}$ and $t_b=\sqrt{1-R_b}$ . For a natural number $L$ and real $N\ge0$ , define $\psi_{L,N}$ on $\mathbb N^L\times\mathbb N^L$ by coefficients

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

regarded as an element of $\ell^2$ when these coefficients are square-summable and replaced by zero otherwise. 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\le n\text{ componentwise},\\ 0,&\text{otherwise}, \end{cases} \quad K_{b,L,N}((p,n),(q,v)) =\sum_{k\in\mathbb N^L} \psi_{L,N}(p,n+k)A_b(n+k,k) \overline{\psi_{L,N}(q,v+k)A_b(v+k,k)}.

For kernels $K,L'$ on $X$ , a resolution is a representation $K(x,y)=\sum_j a_j u_j(x)\overline{u_j(y)}$ by nonnegative summable weights of sum one and vectors in $\ell^2(X;\mathbb C)$ , normalized on positive weights and orthogonal for distinct positive-weight indices; zero-weight vectors are unrestricted. Write $h(a,s)=0$ if $a=0$ , and $h(a,s)=a^s$ , using real powers, otherwise. Define

C_s(K,L')= \sup_{\substack{(a_j,u_j)\text{ resolves }K\$b_j,v_j)\text{ resolves }L'}} \sum_{j,k\ge0}h(a_j,s)h(b_k,1-s)|\langle u_j,v_k\rangle|^2, \qquad C(K,L')=\inf_{s\in[0,1]}C_s(K,L').

In particular, the zero-weight convention applies even at exponent zero. Define (F(K,L') $as the supremum of$ |\langle z,w\rangle|^2 $over unit vectors in$ \ell^2(X\times\mathbb N;\mathbb C) $whose respective marginals$ \sum_e z(x,e)\overline{z(y,e)} $and$ \sum_e w(x,e)\overline{w(y,e)} $equal$ K,L' $. Define$ P(K,L') $as the infimum, over the two resolutions above and bounded complex-linear$ E=E^* $with$ 0\le\operatorname{Re}\langle v,Ev\rangle\le|v|^2 $for every$ v$, of

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

All these extrema are the specified real infima and suprema, with empty defining sets assigned zero. Abbreviate their values on $K_{0,L,N},K_{1,L,N}$ by $C_{s,L,N},C_{L,N},F_{L,N},P_{L,N}$ . For every real $N>0$ , put

a=\frac{(1-R_0)N+1}{(1-R_1)N+1},\quad b=\frac{1-R_0}{1-R_1},\quad C=\frac{((1-r_0r_1)N+1)^2}{(1-R_0)N+1},\quad D=(1-R_1)N,

and

s_*= \begin{cases} 0,&D\log b-C\log a\ge0,\\[2pt] \displaystyle\min\!\left\{1,\frac{\log\!\left(\frac{C\log a}{D\log b}\right)} {\log(b/a)}\right\},&D\log b-C\log a<0. \end{cases}

The declaration asserts $1<a<b$ , $0<D<C$ , and, for every $s\in[0,1]$ ,

Ca^s-Db^s>0,\qquad C_{s,1,N}=(Ca^s-Db^s)^{-1},\qquad C_{s,M,N}=(C_{s,1,N})^M.

It further asserts $s_*\in[0,1]$ , $C_{s_*,M,N}\le C_{s,M,N}$ for every $s\in[0,1]$ , $C_{M,N}=C_{s_*,M,N}$ , and

P_{M,N}\le\frac12(Ca^{s_*}-Db^{s_*})^{-M},

where the last exponent is an integer power. Separately, at $N=0$ , it asserts $F_{M,0}=1$ , $C_{M,0}=1$ , and $P_{M,0}=1/2$ .

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