Gaussian cross entropy in general quadrature conventions

Open

QAlgorithms.Papers.Independent.Intakethird100.P17.gaussian_cross_entropy

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

prove2quantum

Let $n\ge0$ , $\kappa>0$ , and let $\rho_j=\rho(\sigma_j,u_j)$ , $j=1,2$ , be normalized finite-energy Gaussian densities on the full $n$ -mode oscillator space, with arbitrary finite means $u_j\in\mathbb R^{2n}$ and centered half-anticommutator covariances $\sigma_j$ . The quadratures satisfy $[q,q^T]=i\Omega/\kappa$ , where $\Omega$ is the direct sum of the canonical two-dimensional antisymmetric form. Assume each symplectic eigenvalue of each covariance is strictly greater than $1/(2\kappa)$ . Put $\delta=u_2-u_1$ and $G_2=2i\Omega\operatorname{arcoth}(2\kappa\sigma_2 i\Omega)$ . Then the cross entropy is finite and

-\operatorname{Tr}(\rho_1\log_2\rho_2) =\Sigma_\kappa(\sigma_1,\sigma_2,\delta) :=\frac{\ln\det(\kappa\sigma_2+i\Omega/2)+\kappa\operatorname{tr}(\sigma_1G_2)+\kappa\delta^TG_2\delta}{2\ln2}.

A simultaneous displacement of both states gives the centered calculation in (A18). The identity does not require commuting covariance matrices or commuting density operators.

Formalization Note Cross entropy is independently computed from bounded support-log cutoffs of the actual density operator. The theorem asserts convergence to the displayed expression; the matrix inverse-coth series also has an explicit convergence conclusion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P17

Formal statement

noncomputable section

open Filter

open scoped BigOperators ENNReal ComplexOrder Topology Matrix

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P17

open QAlgorithms.Papers.Independent.Claimed50.P30
  (ModeOperator Quadrature PhaseVector numberKet trace TraceSummable
   FockWeylSystem GaussianMoments canonicalOmega)

open QAlgorithms.Papers.Independent.Dependency50.P13 (IsTraceClass relativeEntropy)

open QAlgorithms.Papers.Independent.Next46.P17 (raisingCoefficient)

/-- arXiv:1808.00608v4, Appendix A, PDF p.7, (A18)--(A19).
Arbitrary finite means; strict Gibbs domain for both covariances. The common
displacement leaves delta=u2-u1; no commuting-covariance premise is imposed. -/
theorem gaussian_cross_entropy {n : ℕ}
    (W : FockWeylSystem n) (kappa : ℝ) (hkappa : 0 < kappa)
    (rho1 rho2 : ModeOperator n) (u1 u2 : PhaseVector n)
    (sigma1 sigma2 : Matrix (Quadrature n) (Quadrature n) ℝ)
    (h1 : GaussianInConvention W kappa rho1 u1 sigma1)
    (h2 : GaussianInConvention W kappa rho2 u2 sigma2)
    (hs1 : StrictGibbsCovariance kappa sigma1)
    (hs2 : StrictGibbsCovariance kappa sigma2) :
    Summable (gibbsSeriesTerm kappa sigma1) ∧
    Summable (gibbsSeriesTerm kappa sigma2) ∧
    (∀ k, TraceSummable (rho1.comp (oscillatorLogCutoff rho2 k))) ∧
    Tendsto (crossEntropyCutoff rho1 rho2) atTop
      (nhds (gaussianSigma kappa sigma1 sigma2 (u2 - u1))) ∧
    oscillatorCrossEntropy rho1 rho2 = gaussianSigma kappa sigma1 sigma2 (u2 - u1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P17

end

Source

Tight bounds for private communication over bosonic Gaussian channels based on teleportation simulation with optimal finite resources, arXiv:1808.00608v4, PDF p. 7, Appendix A Eqs. (A18)–(A19): Gaussian cross entropy in κ conventions

Read-back

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

For every natural number $n$ , put $F=\{0,\ldots,n-1\}\to\mathbb N$ , $\mathcal H_n=\ell^2(F;\mathbb C)$ , $J=\{0,\ldots,n-1\}\times\{0,1\}$ , and let $e_j$ be the standard basis. Suppose $W(\xi)$ , for real $\xi\in\mathbb R^J$ , is a unitary bounded operator with

(W(\xi)e_j)_i=\prod_{r=0}^{n-1}\mathcal D_{-\xi_{(r,1)}+i\xi_{(r,0)}}(i_r,j_r), \quad \mathcal D_z(a,b)=e^{-|z|^2/2}\sqrt{a!\,b!} \sum_{\ell=0}^{\min(a,b)} \frac{z^{a-\ell}(-\overline z)^{b-\ell}} {\ell!(a-\ell)!(b-\ell)!}.

Let $\kappa>0$ , let $\rho_1,\rho_2$ be bounded complex linear operators on $\mathcal H_n$ , let $u_1,u_2\in\mathbb R^J$ , and let $\sigma_1,\sigma_2$ be real $J\times J$ matrices. For each $r=1,2$ , assume that $\rho_r x=\sum_\ell\langle v_\ell,x\rangle w_\ell$ for some sequences with $\sum_\ell\|v_\ell\|\|w_\ell\|<\infty$ , that $\rho_r^*=\rho_r$ and $\operatorname{Re}\langle x,\rho_rx\rangle\ge0$ for all $x$ , that its number-basis trace series is summable and equals $1$ , and that $\sum_j(\sum_mj_m)\operatorname{Re}\langle e_j,\rho_re_j\rangle$ is summable. Let $\Omega_{(m,0),(m,1)}=1$ , $\Omega_{(m,1),(m,0)}=-1$ , with all other entries zero. Assume for each $r$ that $2\kappa\sigma_r$ is symmetric and positive definite, that $2\kappa\sigma_r+i\Omega$ is positive semidefinite, and that for every real $\xi$ the trace series of $\rho_rW(\xi)$ is summable and

\sum_j\langle e_j,\rho_rW(\xi)e_j\rangle =\exp\!\left( -\kappa\sum_{a,b}\xi_a(\sigma_r)_{ab}\xi_b +i\sqrt{2\kappa}\sum_a(u_r)_a\xi_a \right).

Assume additionally, for both $r$ , that $\sigma_r$ is symmetric and positive definite and that the complex matrix $\kappa\sigma_r+\frac{i}{2}\Omega$ is positive definite. Define

B_r=2\kappa\sigma_r(i\Omega),\qquad H_{r,k}=\frac{(B_r^{-1})^{2k+1}}{2k+1},\qquad G_2=\operatorname{Re}\!\left(2i\Omega\sum_{k=0}^{\infty}H_{2,k}\right)

entrywise, and put

\delta=u_2-u_1,\qquad S= \frac{ \log\!\left(\operatorname{Re}\det(\kappa\sigma_2+\tfrac{i}{2}\Omega)\right) +\kappa\operatorname{tr}(\sigma_1G_2) +\kappa\sum_{a,b}\delta_a(G_2)_{ab}\delta_b }{2\log 2}.

Then both matrix series $\sum_kH_{1,k}$ and $\sum_kH_{2,k}$ are summable. For every natural number $k$ , the number-basis trace series of $\rho_1 f_k(\rho_2)$ is summable, where $f_k(x)=\log(\max\{x,1/(k+1)\})/\log2$ is applied by the real continuous functional calculus. Moreover,

-\operatorname{Re}\sum_j\langle e_j,\rho_1 f_k(\rho_2)e_j\rangle \longrightarrow S \quad\text{as }k\to\infty,

and the value selected by the total filter-limit definition of this cutoff sequence equals $S$ . No assumption $n>0$ is present, so the zero-mode case is included.

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