Average Gaussian-prior coherent-state fidelity

Open

QAlgorithms.Papers.Independent.Intakethird100.P89.averageCoherentFidelity

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\lambda>0$ , $\tau\ge0$ , and let $\Phi$ be a zero-displacement phase-insensitive Gaussian channel with noise $y\ge|1-\tau|$ on the complete oscillator space. The coherent projectors are normalized trace-class states, their channel outputs have bounded operator realizations, and the prior $P_\lambda(\alpha)=(\lambda/\pi)e^{-\lambda|\alpha|^2}$ is integrable with integral one. Pointwise,

\langle\alpha|\Phi(|\alpha\rangle\langle\alpha|)|\alpha\rangle=\frac{2\exp\!\left[-2(1-\sqrt\tau)^2|\alpha|^2/(1+y+\tau)\right]}{1+y+\tau}.

The prior-weighted overlap is integrable and

\overline F_\lambda=\int_{\mathbb C}P_\lambda(\alpha)\langle\alpha|\Phi(|\alpha\rangle\langle\alpha|)|\alpha\rangle\,d^2\alpha=\frac{2\lambda}{2(1-\sqrt\tau)^2+\lambda(1+y+\tau)}.

This is squared pure-state fidelity. The source's $Q_{\Phi(|\alpha\rangle\langle\alpha|)}(\alpha)$ is the pointwise overlap divided by $\pi$ , including dependence on $\alpha$ through the input state. No resource-entanglement assumption is needed for this channel identity.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P89

Formal statement

noncomputable section

open MeasureTheory Filter

open scoped BigOperators ENNReal Topology ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P89

open QAlgorithms.Papers.Independent.Dependency50.P33
  (State IsDensity IsTraceClassChannel tensorApply traceSize)

open QAlgorithms.Papers.Independent.Dependency50.P39
  (coherentKet coherentCoefficient operatorOfMatrix husimiQ HasFockMatrix CoherentRealized)

open QAlgorithms.Papers.Independent.Frontier30.P14 (weylCharacteristic)

open QAlgorithms.Papers.Independent.Claimed50.P19
  (Cov FockIndex DensityKernel PhysicalCovariance CharacteristicSummable
   multimodeWeylTrace covarianceCharacteristicValue standardFormCovariance)

open QAlgorithms.Papers.Independent.Frontier30.P08 (QuadratureIndex)

open QAlgorithms.Papers.Independent.Gap48.P26 (PhaseInsensitive coherentKernel)

open QAlgorithms.Entanglement (partialTransposeFirst)

/-- PDF p.4, (11)--(12): actual squared-overlap integral and pointwise
Q/overlap identity. Integrability, prior normalization, coherent normalization
and bounded output realization are conclusions, not assumed formulae. -/
theorem averageCoherentFidelity (lambda tau y : ℝ) (Phi : OscillatorChannel)
    (hlambda : 0 < lambda) (htau : 0 ≤ tau) (hPhi : PhaseInsensitive Phi tau y) :
    CoherentRealized ∧
    Integrable (priorDensity lambda) ∧ (∫ alpha : ℂ, priorDensity lambda alpha) = 1 ∧
    (∀ alpha : ℂ, IsDensity (coherentKernel alpha) ∧
      HasFockMatrix (operatorOfMatrix (Phi (coherentKernel alpha))) (Phi (coherentKernel alpha)) ∧
      teleportedCoherentOverlap Phi alpha =
        2 * Real.exp (-2 * (1 - Real.sqrt tau) ^ 2 * Complex.normSq alpha / (1 + y + tau)) /
          (1 + y + tau)) ∧
    Integrable (fun alpha => priorDensity lambda alpha * teleportedCoherentOverlap Phi alpha) ∧
    gaussianPriorFidelity lambda Phi = phaseInsensitiveFidelityFormula lambda tau y := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P89

end

Source

Optimal continuous variable quantum teleportation with limited resources, arXiv:1705.03017v5, PDF p. 4, Average coherent-state fidelity of a physical phase-insensitive channel, Eq. (12)

Read-back

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

Let $\lambda,\tau,y\in\mathbb R$ with $\lambda>0$ and $\tau\ge0$ , and let $\Phi$ be a function on complex kernels on $\mathbb N$ . A trace-class kernel on $I$ here admits $X_{ij}=\sum_k u_k(i)\overline{v_k(j)}$ with $u_k,v_k\in\ell^2(I;\mathbb C)$ and $\sum_k\|u_k\|\|v_k\|<\infty$ ; a density kernel additionally has real nonnegative finite quadratic forms and a summable real diagonal of sum one. Assume $\Phi$ preserves trace-class kernels, is additive and complex homogeneous on them, and preserves density kernels under every finite first-factor ampliation, with the dimension-zero condition vacuous. Assume also $|\tau-1|\le y$ and, for every one-mode density kernel $S$ and $z\in\mathbb C$ ,

\chi_{\Phi(S)}(z)=\chi_S(\sqrt\tau z)e^{-y|z|^2/2},\qquad \chi_X(z)=\sum_m\sum_nX_{mn}D_{nm}(z),

where

D_{mn}(z)=e^{-|z|^2/2}\sqrt{m!n!} \sum_{j=0}^{\min(m,n)} \frac{z^{m-j}(-\overline z)^{n-j}}{j!(m-j)!(n-j)!}.

Set $c_\alpha(n)=e^{-|\alpha|^2/2}\alpha^n/\sqrt{n!}$ and $P_\alpha(m,n)=c_\alpha(m)\overline{c_\alpha(n)}$ . Let $h_\alpha$ be the chosen vector in $\ell^2(\mathbb N;\mathbb C)$ with these coefficients if one exists, and zero otherwise; let $O(X)$ be the chosen bounded operator with matrix $X$ if one exists, and zero otherwise. Then, for every $\alpha$ , $h_\alpha(n)=c_\alpha(n)$ for all $n$ and $\|h_\alpha\|=1$ . The function $p_\lambda(\alpha)=(\lambda/\pi)e^{-\lambda|\alpha|^2}$ is Lebesgue integrable on $\mathbb C$ and has integral one. For every $\alpha$ , $P_\alpha$ is a density kernel, the operator $O(\Phi(P_\alpha))$ actually has matrix $\Phi(P_\alpha)$ , and

Q_\Phi(\alpha):= \operatorname{Re}\langle h_\alpha,O(\Phi(P_\alpha))h_\alpha\rangle = \frac{2\exp\!\left(-\dfrac{2(1-\sqrt\tau)^2|\alpha|^2}{1+y+\tau}\right)} {1+y+\tau}.

The product $p_\lambda Q_\Phi$ is integrable, and its integral is

\int_{\mathbb C}p_\lambda(\alpha)Q_\Phi(\alpha)\,d\alpha = \frac{2\lambda}{2(1-\sqrt\tau)^2+\lambda(1+y+\tau)}.

The assumptions include $\tau=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