Signal-energy bound on the Chernoff exponent

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.chernoff_exponent

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 additionally $R_1<1$ , and let a normalized pure probe have finite mean signal energy $N_s$ . Then $0<\mu<1$ and $Q(\psi)>0$ . With natural logarithms and $\xi=-\ln Q(\psi)$ ,

\xi\le-2N_s\ln\mu=\ln\bigl(\mu^{-2N_s}\bigr).

For each positive integer $L$ , the normalized experiment consisting of $L$ independent copies also satisfies

P_e(\psi^{\otimes L})\ge\frac14\mu^{2N_sL}.

These bounds control copy asymptotics; the identification of $\xi$ with the limiting optimal-error exponent is cited background, equation (55), rather than a new theorem of this paper.

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

/-- Chernoff exponent and finite-copy bound, PDF p.7, (56)–(57).
Natural logarithms are used; R1<1 excludes a log-zero/infinite-exponent endpoint.
The identification with the asymptotic opticalError exponent (55) is cited background [18]. -/
theorem chernoff_exponent {M J : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (hloss : (c true).reflectance < 1)
    (psi : Hilbert (Occupation (Fin J) × Occupation (Fin M))) (hpsi : ‖psi‖=1)
    (N : ℝ) (hN : HasSignalEnergy psi N) :
    0 < splitterOverlap c ∧ splitterOverlap c < 1 ∧ 0 < outputChernoff c psi ∧
    -Real.log (outputChernoff c psi) ≤ -2*N*Real.log (splitterOverlap c) ∧
    ∀ L : ℕ, 0 < L → ‖opticalCopies psi L‖=1 ∧
      Real.rpow (splitterOverlap c) (2*N*(L : ℝ))/4 ≤ outputError c (opticalCopies psi L) := 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. 7, chernoff-exponent

Read-back

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

Let $M,J\in\mathbb N$ with $M>0$ , and let the two splitters $c$ have reflectances $R_b\in[0,1]$ , phases $\phi_b$ , $R_0\le R_1$ , unequal fields $\sqrt{R_0}e^{i\phi_0}\ne\sqrt{R_1}e^{i\phi_1}$ , and $\phi_0=\phi_1=0$ ; additionally assume $R_1<1$ . Put $r_b=\sqrt{R_b}$ , $t_b=\sqrt{1-R_b}$ , and $o=r_0r_1+t_0t_1$ . Let $\psi\in\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ have norm $1$ , and let $N\in\mathbb R$ be nonnegative with $n\mapsto nP_n$ summable and $\sum_n nP_n=N$ , where $P_n=\sum_{q:\,\sum_mq_m=n}\sum_i|\psi(i,q)|^2$ . For any probe $\chi$ with $m$ signal modes, define $a_b(q,k)=\prod_{\ell=1}^m\sqrt{\binom{q_\ell}{k_\ell}}r_b^{q_\ell-k_\ell}t_b^{k_\ell}$ if $k\le q$ coordinatewise, and $0$ otherwise; its returned kernels are $K_b^\chi(x,y)=\sum_k z_{b,k}^\chi(x)\overline{z_{b,k}^\chi(y)}$ , where $z_{b,k}^\chi(i,q)=\chi(i,q+k)a_b(q+k,k)$ . A resolution of a kernel $K$ means $K(x,y)=\sum_a p_a u_a(x)\overline{u_a(y)}$ , with $u_a\in\ell^2$ , nonnegative summable $p_a$ , $\sum_a p_a=1$ , unit $u_a$ for positive weights, and orthogonality between distinct vectors having positive weights; zero-weight vectors are unrestricted. For two kernels define

C_s(K_0,K_1)= \sup_{\substack{(p_a,u_a)\text{ resolves }K_0\$q_b,v_b)\text{ resolves }K_1}} \sum_{(a,b)\in\mathbb N^2} f_s(p_a)f_{1-s}(q_b)|\langle u_a,v_b\rangle|^2, \qquad C(K_0,K_1)=\inf_{0\le s\le1}C_s(K_0,K_1),

where (f_t(p)=0 $when$ p=0 $and$ f_t(p)=p^t $, the real power, otherwise; thus zero weights contribute$ 0 $even when the exponent is$ 0 $. Define$ e(K_0,K_1) $as the infimum over these resolutions and bounded complex-linear effects$ E $, satisfying$ \langle u,Ev\rangle=\overline{\langle v,Eu\rangle} $and$ 0\le\operatorname{Re}\langle v,Ev\rangle\le|v|^2 $, of$ \frac12\sum_a p_a(1-\operatorname{Re}\langle u_a,Eu_a\rangle)+\frac12\sum_b q_b\operatorname{Re}\langle v_b,Ev_b\rangle $. These are real suprema and infima, with value$ 0 $on empty defining sets; infinite sums have value$ 0$ if not summable. Then

0<o<1,\qquad 0<C(K_0^\psi,K_1^\psi),\qquad -\log C(K_0^\psi,K_1^\psi)\le-2N\log o.

Moreover, for every natural number $L>0$ , form the coefficient function

g_L(i,q)=\prod_{\ell=0}^{L-1}\psi\bigl(i_\ell,(q_{\ell M+m})_{m=0}^{M-1}\bigr), \quad i\in(\mathbb N^J)^L,\quad q\in\mathbb N^{LM},

and let $\psi^{[L]}$ be this function as an $\ell^2$ vector if it is square summable, and the zero vector otherwise. The assertion also gives

\|\psi^{[L]}\|=1, \qquad \frac{o^{\,2NL}}4\le e(K_0^{\psi^{[L]}},K_1^{\psi^{[L]}}).

The statement allows $J=0$ , $N=0$ , and $R_0=0$ , but its conclusion about copies is only for $L>0$ .

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