Fidelity and common-exponent Chernoff product laws

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.product_laws

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.

Let $|\Psi\rangle=\bigotimes_{m=1}^M|\psi_m\rangle$ , where each normalized pure factor has one signal mode and an arbitrary finite retained idler register. The factors need not be identical or NDS. The grouped product is normalized, and for each common $s\in[0,1]$ ,

\mathcal F(\Psi)=\prod_{m=1}^M\mathcal F(\psi_m),\qquad Q_s(\Psi)=\prod_{m=1}^M Q_s(\psi_m).

These identities reduce a product experiment to its individual factors. They do not assert multiplicativity after independently minimizing the exponent in each factor.

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

/-- Product laws for arbitrary, possibly different and non-NDS, pure factors,
PDF p.6, (46)–(47). The same s is used in every factor; optimized coefficients
are not asserted to multiply. Equation (47)'s missing factor subscript is restored. -/
theorem product_laws {M : ℕ} (hM : 0 < M) (c : Channels) (hc : ValidSplitters c)
    (J : Fin M → ℕ) (psi : ∀ m, Hilbert (Occupation (Fin (J m)) × Occupation (Fin 1)))
    (hpsi : ∀ m, ‖psi m‖ = 1) :
    ‖productOpticalProbe J psi‖ = 1 ∧
    outputFidelity c (productOpticalProbe J psi) = ∏ m, outputFidelity c (psi m) ∧
    ∀ s ∈ Set.Icc (0 : ℝ) 1,
      outputChernoffAt c (productOpticalProbe J psi) s = ∏ m, outputChernoffAt c (psi m) s := 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. 6, product-laws

Read-back

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

Let $M\in\mathbb N$ with $M>0$ . Let two splitters have reflectances $R_b\in[0,1]$ , phases $\theta_b\in\mathbb R$ , $r_b=\sqrt{R_b}$ , and $t_b=\sqrt{1-R_b}$ , satisfying $R_0\le R_1$ and $r_0e^{i\theta_0}\ne r_1e^{i\theta_1}$ . For each $m\in\{0,\ldots,M-1\}$ , choose $J_m\in\mathbb N$ , possibly zero, and a norm-one vector $\psi_m\in\ell^2(\mathbb N^{J_m}\times\mathbb N;\mathbb C)$ , identifying a one-mode occupation with its single natural-number entry. Define $\Psi\in\ell^2((\prod_m\mathbb N^{J_m})\times\mathbb N^M;\mathbb C)$ from the function

\Psi((i_m)_m,n)=\prod_m\psi_m(i_m,n_m),

using that function if it is square-summable and zero otherwise. For any probe $\phi$ with a finite set of signal modes, define $L_b(n,k)=\prod_m\sqrt{\binom{n_m}{k_m}}e^{in_m\theta_b}r_b^{n_m-k_m}t_b^{k_m}$ when $k\le n$ componentwise and zero otherwise, and define its returned kernels by $\rho_b^\phi(x,y)=\sum_k g_{b,k}^\phi(x)\overline{g_{b,k}^\phi(y)}$ , where $g_{b,k}^\phi(i,p)=\phi(i,p+k)L_b(p+k,k)$ . Write $F(\phi)$ for the supremum of $|\langle z,w\rangle|^2$ over unit square-summable vectors on the probe’s output labels times $\mathbb N$ , with marginals $\sum_e z(x,e)\overline{z(y,e)}=\rho_0^\phi(x,y)$ and $\sum_e w(x,e)\overline{w(y,e)}=\rho_1^\phi(x,y)$ . A resolution $(a_n,u_n)$ of a kernel means summable nonnegative weights of sum $1$ , vectors unit at positive weights and orthogonal at distinct positive weights, and the entrywise representation $K(x,y)=\sum_n a_nu_n(x)\overline{u_n(y)}$ ; zero-weight vectors are unrestricted. Write

Q_s(\phi)=\sup_{(a,u),(b,w)} \sum_{n,l\in\mathbb N}h(a_n,s)h(b_l,1-s) |\langle u_n,w_l\rangle|^2,

where the resolutions are of $\rho_0^\phi,\rho_1^\phi$ , and $h(p,t)=0$ if $p=0$ and $h(p,t)=p^t$ otherwise. Empty defining sets for these real suprema give value $0$ . The theorem asserts

\|\Psi\|=1,\qquad F(\Psi)=\prod_m F(\psi_m),\qquad Q_s(\Psi)=\prod_m Q_s(\psi_m)\quad\text{for every }s\in[0,1].

There is no additional orthogonality condition on the input probes, and the endpoints $s=0,1$ use the stated zero-weight convention.

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