Pure coherent probes attain the classical optimum

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.classical_optimum

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 $\nu$ be any probability measure on joint signal and idler coherent amplitudes. Allow arbitrary classical correlations, including Dirac masses. Suppose the signal energy $\sum_m|\alpha_m|^2$ is integrable and its $\nu$ -mean is $N_s\ge0$ . The corresponding classical mixture satisfies

P_e(\nu)\ge\frac{1-\sqrt{1-e^{-(r_1-r_0)^2N_s}}}{2}.

A pure product coherent probe of signal energy $N_s$ attains equality. No constraint is placed on idler energy.

This classical optimum combines the coherent error formula with the bound explicitly credited to Theorem 1 of reference [3]. It concerns vacuum background.

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

/-- Optimal classical performance, PDF p.8, combining (61) with the explicitly
cited Theorem 1 of [3]. Arbitrary correlated coherentOpticalProbe-lossAmplitude probability measures
and Dirac masses are included; only mean SIGNAL energy is constrained. -/
theorem classical_optimum {M J : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c)
    (nu : Measure ((Fin J → ℂ) × (Fin M → ℂ))) [IsProbabilityMeasure nu]
    (N : ℝ) (hN : 0 ≤ N) (hint : Integrable (fun a => coherentEnergy a.2) nu)
    (henergy : (∫ a, coherentEnergy a.2 ∂nu)=N) :
    lowerError (Real.exp (-coherentExponent c*N)) ≤
      opticalError (classicalReturned (c false) nu) (classicalReturned (c true) nu) ∧
    ∃ (beta : Fin J → ℂ) (alpha : Fin M → ℂ), coherentEnergy alpha=N ∧
      outputError c (coherentOpticalProbe beta alpha)=lowerError (Real.exp (-coherentExponent c*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. 8, classical-optimum

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 $c$ be a pair of splitters with reflectances $R_b\in[0,1]$ and phases $\phi_b$ , satisfying $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$ . Let $\nu$ be a probability measure on $\mathbb C^J\times\mathbb C^M$ , and let $N\in\mathbb R$ satisfy $N\ge0$ , integrability of $(\beta,\alpha)\mapsto E_\alpha=\sum_m|\alpha_m|^2$ , and $\int E_\alpha\,d\nu=N$ . Put $d=(\sqrt{R_1}-\sqrt{R_0})^2$ , define $h_z(n)=e^{-|z|^2/2}z^n/\sqrt{n!}$ , and let $\psi_{\beta,\alpha}$ be the function $(i,q)\mapsto\prod_jh_{\beta_j}(i_j)\prod_mh_{\alpha_m}(q_m)$ as an $\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ vector if square summable, and $0$ otherwise. Define

G_b(x,y)=\int \psi_{\beta,\sqrt{R_b}\alpha}(x)\, \overline{\psi_{\beta,\sqrt{R_b}\alpha}(y)}\,d\nu(\beta,\alpha).

For any probe $\chi$ , also define $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)$ and $a_b(q,k)=\prod_m\sqrt{\binom{q_m}{k_m}}(\sqrt{R_b})^{q_m-k_m}(\sqrt{1-R_b})^{k_m}$ for $k\le q$ , and $0$ otherwise. A resolution of a kernel $K$ is $K(x,y)=\sum_a p_a u_a(x)\overline{u_a(y)}$ , with nonnegative summable weights of sum $1$ , unit $\ell^2$ vectors at positive weights, and orthogonality between distinct positive-weight vectors; zero-weight vectors are unrestricted. Let $e(K,H)$ be the real infimum over resolutions $(p_a,u_a),(q_b,v_b)$ of $K,H$ and bounded complex-linear effects $A$ satisfying $\langle u,Av\rangle=\overline{\langle v,Au\rangle}$ and $0\le\operatorname{Re}\langle v,Av\rangle\le\|v\|^2$ , of $\frac12\sum_a p_a(1-\operatorname{Re}\langle u_a,Au_a\rangle)+\frac12\sum_b q_b\operatorname{Re}\langle v_b,Av_b\rangle$ ; the empty defining set has infimum $0$ . The assertion is

\frac{1-\sqrt{1-e^{-dN}}}{2}\le e(G_0,G_1),

and there exist $\beta\in\mathbb C^J$ and $\alpha\in\mathbb C^M$ such that

\sum_m|\alpha_m|^2=N, \qquad e(K_0^{\psi_{\beta,\alpha}},K_1^{\psi_{\beta,\alpha}}) =\frac{1-\sqrt{1-e^{-dN}}}{2}.

The statement allows $J=0$ , $N=0$ , and reflectance endpoints. Infinite sums are total sums, equal to $0$ when not summable, and the kernel integrals displayed above are the entrywise complex integrals appearing in the definition.

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