Globally optimized gain with a fixed pure TMSS

Open

QAlgorithms.Papers.Independent.Intakethird100.P89.optimizedTMSSGain

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

prove2quantum

Let $\lambda>0$ , $r\ge0$ , both finite. Fix the normalized pure TMSS with covariance blocks $A=B=\cosh(2r)I$ , $C=-\sinh(2r)\sigma_z$ , logarithmic negativity $2r$ , and finite per-mode photon number $\sinh^2r$ . For every gain $g>0$ its BK map exists on every input density and is the phase-insensitive channel with

\tau=g^2,\qquad y=(1+g^2)\cosh(2r)-2g\sinh(2r).

The actual Gaussian-prior average fidelity, globally optimized over all positive gains, is attained at

g_{\rm opt}=\frac{2+\lambda\sinh(2r)}{2+\lambda+\lambda\cosh(2r)}>0,\qquad \overline F_{\rm TMSS}=\frac{\operatorname{sech}^2r+\lambda}{2+\lambda-2\tanh r}.

The attainable fidelity set has the displayed greatest element, and its independently defined supremum equals that value. The resource is fixed before the gain and before all input states.

This optimizes gain at fixed squeezing, unlike (10), which minimizes squeezing for a fixed channel.

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, (16): a fixed normalized TMSS precedes the optimization over
all g>0. The closed value is globally maximal and is attained at the stated gain. -/
theorem optimizedTMSSGain (lambda r : ℝ) (hlambda : 0 < lambda) (hr : 0 ≤ r) :
    0 < tmssOptimalGain lambda r ∧
    IsGreatest (tmssValues lambda r) (tmssClosedForm lambda r) ∧
    tmssOptimum lambda r = tmssClosedForm lambda r ∧
    (∃ rho : State (ℕ × ℕ),
      rho.coefficients = tmssKernel r ∧
      CenteredResource rho (standardFormCovariance (Real.cosh (2 * r)) (Real.cosh (2 * r))
        (-Real.sinh (2 * r)) (Real.sinh (2 * r))) ∧
      traceSize (partialTransposeFirst rho.coefficients) = ENNReal.ofReal (Real.exp (2 * r)) ∧
      twoModeMeanPhotonEnergy rho = ENNReal.ofReal (Real.sinh r ^ 2) ∧ twoModeMeanPhotonEnergy rho < ⊤ ∧
      (∀ g : ℝ, 0 < g → ∃ Phi : OscillatorChannel,
        IsBK rho g Phi ∧ PhaseInsensitive Phi (g ^ 2) (tmssNoise g r) ∧
        gaussianPriorFidelity lambda Phi = phaseInsensitiveFidelityFormula lambda (g ^ 2) (tmssNoise g r)) ∧
      (∃ Phi : OscillatorChannel, IsBK rho (tmssOptimalGain lambda r) Phi ∧
        gaussianPriorFidelity lambda Phi = tmssClosedForm lambda r)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P89

end

Source

Optimal continuous variable quantum teleportation with limited resources, arXiv:1705.03017v5, PDF p. 4, Optimized-gain fidelity with a fixed TMSS resource, Eq. (16)

Read-back

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

For every real $\lambda>0$ and $r\ge0$ , define

g_*=\frac{2+\lambda\sinh(2r)}{2+\lambda+\lambda\cosh(2r)}, \qquad L=\frac{\cosh(r)^{-2}+\lambda}{2+\lambda-2\tanh r}.

Then $g_*>0$ . To specify the value set, write $H_I=\ell^2(I;\mathbb C)$ ; a trace-class kernel admits $X_{ij}=\sum_k u_k(i)\overline{v_k(j)}$ with $u_k,v_k\in H_I$ and $\sum_k\|u_k\|\|v_k\|<\infty$ , and a density kernel additionally has real nonnegative finite quadratic forms and a summable real diagonal of sum one. A channel here preserves trace-class kernels, is additive and complex homogeneous on them, and preserves density kernels under each finite first-factor ampliation, including the vacuous dimension-zero test. Put

t_r(a)=\mathbf1_{a_0=a_1}\frac{(-\tanh r)^{a_0}}{\cosh r}, \quad 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)!},

\chi_X(z)=\sum_m\sum_nX_{mn}D_{nm}(z),\qquad \chi_R^{(2)}(v)=\sum_a\sum_bR_{ab} \prod_{j=0}^1D_{b_ja_j}\!\left(\frac{-v_{j,1}+iv_{j,0}}{\sqrt2}\right).

Set $c_\alpha(n)=e^{-|\alpha|^2/2}\alpha^n/\sqrt{n!}$ and $P_\alpha=c_\alpha c_\alpha^*$ ; let $h_\alpha$ be a chosen square-summable vector with coefficients $c_\alpha$ , or zero if none exists, and let $O(X)$ be a chosen bounded operator with matrix $X$ , or zero if none exists. Define

\mathcal F_\lambda(\Phi)= \int_{\mathbb C}\frac{\lambda}{\pi}e^{-\lambda|\alpha|^2} \operatorname{Re}\langle h_\alpha,O(\Phi(P_\alpha))h_\alpha\rangle\,d\alpha.

Consider all these real values for which there exist a two-mode density kernel $R$ with $R_{ab}=t_r(a)\overline{t_r(b)}$ , a real $g>0$ , and a channel $\Phi$ such that, for every one-mode density kernel $S$ and $z\in\mathbb C$ ,

\chi_{\Phi(S)}(z)=\chi_S(gz)\, \chi_R^{(2)}(\sqrt2g\operatorname{Im}z,\sqrt2g\operatorname{Re}z, \sqrt2\operatorname{Im}z,-\sqrt2\operatorname{Re}z).

The number $L$ is a member of this value set, is at least every member, and equals its real supremum. Furthermore, there exists such a density kernel $R$ whose centered covariance is

V= \begin{pmatrix} \cosh(2r)&0&-\sinh(2r)&0\\ 0&\cosh(2r)&0&\sinh(2r)\\ -\sinh(2r)&0&\cosh(2r)&0\\ 0&\sinh(2r)&0&\cosh(2r) \end{pmatrix}.

Explicitly, $V$ is symmetric positive definite, $V+i\operatorname{diag}(J,J)$ is positive semidefinite for $J=\left(\begin{smallmatrix}0&1\\-1&0\end{smallmatrix}\right)$ , every inner and outer series defining $\chi_R^{(2)}(v)$ is summable, and $\chi_R^{(2)}(v)=e^{-v^TVv/4}$ for every real $v$ . With $N(X)$ the extended-nonnegative infimum of the norm-product sums in its trace-class expansions, and $R^\Gamma_{(a,b),(c,d)}=R_{(c,b),(a,d)}$ , this resource satisfies

N(R^\Gamma)=[e^{2r}]_+,\qquad \sum_p\left[\frac{p_0+p_1}{2}\operatorname{Re}R_{pp}\right]_+ =[\sinh^2r]_+<\infty.

Here $[x]_+=\max(x,0)$ in $[0,\infty]$ . For every real gain $g>0$ there exists a channel $\Phi$ satisfying the preceding resource identity and, with

T(g,r)=(1+g^2)\cosh(2r)-2g\sinh(2r),

also satisfying $|g^2-1|\le T(g,r)$ and

\chi_{\Phi(S)}(z)=\chi_S(\sqrt{g^2}\,z)e^{-T(g,r)|z|^2/2}, \qquad \mathcal F_\lambda(\Phi)= \frac{2\lambda}{2(1-\sqrt{g^2})^2+\lambda(1+T(g,r)+g^2)}

for every density $S$ and every $z$ . Finally, there exists a channel satisfying the resource identity at gain $g_*$ and having $\mathcal F_\lambda(\Phi)=L$ . All assertions include $r=0$ ; uniqueness of a maximizing gain or channel is not asserted.

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