Exact coherent-state error and Chernoff coefficient

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.coherent_error

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 the signal coherent amplitudes be $\alpha_m\in\mathbb C$ and the retained idler amplitudes be arbitrary. The full product coherent probe is normalized and has signal energy $N_s=\sum_m|\alpha_m|^2$ . Then

\mathcal F=Q=e^{-(r_1-r_0)^2N_s},\qquad P_e=\frac{1-\sqrt{1-e^{-(r_1-r_0)^2N_s}}}{2}\le\frac12e^{-(r_1-r_0)^2N_s}.

The result depends only on total signal energy, not its distribution among modes. The real field difference is appropriate because the channel phases are aligned.

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

/-- Coherent-state exact error, fidelity and Chernoff coefficient, PDF pp.7–8,
(61),(68), with multimode invariance from footnote [6], p.13. Section IV has
Delta=0; the real field-magnitude difference is therefore legitimate. -/
theorem coherent_error {M J : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (beta : Fin J → ℂ) (alpha : Fin M → ℂ) :
    ‖coherentOpticalProbe beta alpha‖=1 ∧ HasSignalEnergy (coherentOpticalProbe beta alpha) (coherentEnergy alpha) ∧
    outputFidelity c (coherentOpticalProbe beta alpha) = Real.exp (-coherentExponent c * coherentEnergy alpha) ∧
    outputChernoff c (coherentOpticalProbe beta alpha) = Real.exp (-coherentExponent c * coherentEnergy alpha) ∧
    outputError c (coherentOpticalProbe beta alpha) =
      lowerError (Real.exp (-coherentExponent c * coherentEnergy alpha)) ∧
    outputError c (coherentOpticalProbe beta alpha) ≤ Real.exp (-coherentExponent c * coherentEnergy alpha)/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. 7, coherent-error

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$ specify splitters with reflectances $R_b\in[0,1]$ and phases $\phi_b$ , 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$ . For arbitrary $\beta\in\mathbb C^J$ and $\alpha\in\mathbb C^M$ , put $E_\alpha=\sum_m|\alpha_m|^2$ , $d=(\sqrt{R_1}-\sqrt{R_0})^2$ , and $h_z(n)=e^{-|z|^2/2}z^n/\sqrt{n!}$ . Define $\psi_{\beta,\alpha}\in\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ from the coefficient function $(i,q)\mapsto\prod_jh_{\beta_j}(i_j)\prod_mh_{\alpha_m}(q_m)$ if this function is square summable, and as $0$ otherwise. Set $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}$ if $k\le q$ , and $0$ otherwise, and let $K_b(x,y)=\sum_kz_{b,k}(x)\overline{z_{b,k}(y)}$ , where $z_{b,k}(i,q)=\psi_{\beta,\alpha}(i,q+k)a_b(q+k,k)$ . For kernels $K,H$ on $X$ , define $F(K,H)$ to be the real supremum of $|\langle z,w\rangle|^2$ over norm-one $z,w\in\ell^2(X\times\mathbb N;\mathbb C)$ whose respective marginals $\sum_ez(x,e)\overline{z(y,e)}$ and $\sum_ew(x,e)\overline{w(y,e)}$ equal $K,H$ . A resolution is a representation $K(x,y)=\sum_a p_a u_a(x)\overline{u_a(y)}$ , with nonnegative summable weights of sum $1$ , unit vectors at positive weights, and orthogonality for distinct positive-weight vectors; zero-weight vectors are unrestricted. Define $C(K,H)$ to be

\inf_{s\in[0,1]} \sup_{\text{resolutions }(p_a,u_a),(q_b,v_b)} \sum_{a,b}f_s(p_a)f_{1-s}(q_b)|\langle u_a,v_b\rangle|^2,

where $f_t(0)=0$ and $f_t(p)=p^t$ otherwise. Define $e(K,H)$ to be the infimum over these resolutions and bounded complex-linear operators $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 extrema are real and have value $0$ for empty defining sets; infinite sums have value $0$ if not summable. The assertion is that $\|\psi_{\beta,\alpha}\|=1$ , that $P_n=\sum_{q:\,\sum_mq_m=n}\sum_i|\psi_{\beta,\alpha}(i,q)|^2$ has $n\mapsto nP_n$ summable with $\sum_n nP_n=E_\alpha$ and $E_\alpha\ge0$ , and that

F(K_0,K_1)=e^{-dE_\alpha}, \qquad C(K_0,K_1)=e^{-dE_\alpha}, \qquad e(K_0,K_1)=\frac{1-\sqrt{1-e^{-dE_\alpha}}}{2} \le\frac{e^{-dE_\alpha}}2.

No positivity assumption is made on $E_\alpha$ ; $\alpha=0$ , $J=0$ , and reflectance endpoints are included, with empty products equal to $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