Gaussian Umegaki relative entropy with arbitrary means

Open

QAlgorithms.Papers.Independent.Intakethird100.P17.gaussian_relative_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. Covariances are centered half-anticommutator covariances, means $u_j\in\mathbb R^{2n}$ are arbitrary, and $[q,q^T]=i\Omega/\kappa$ for the canonical interleaved symplectic form $\Omega$ . Assume all symplectic eigenvalues of both covariances exceed $1/(2\kappa)$ . For $G_j=2i\Omega\operatorname{arcoth}(2\kappa\sigma_j i\Omega)$ , define

\Sigma_\kappa(S,T,d)=\frac{\ln\det(\kappa T+i\Omega/2)+\kappa\operatorname{tr}(S G_T)+\kappa d^T G_Td}{2\ln2},\qquad G_T=2i\Omega\operatorname{arcoth}(2\kappa T i\Omega).

The independently defined Umegaki relative entropy in bits is finite and satisfies

S(\rho_1\Vert\rho_2)=-\Sigma_\kappa(\sigma_1,\sigma_1,0)+\Sigma_\kappa(\sigma_1,\sigma_2,u_2-u_1).

This general-mean identity specializes to the main-text zero-mean formula when $\kappa=1/2$ .

Formalization Note The left side uses the accepted extended operator relative entropy, converted from nats to bits. Finiteness and nonnegativity are conclusions, so conversion to a real value cannot erase a support failure.

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, (A20).
Equality to independently defined extended Umegaki relative entropy in bits;
its finiteness is concluded. Singular/pure Gibbs boundary is separately deferred. -/
theorem gaussian_relative_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) :
    let D := oscillatorRelativeEntropy rho1 rho2 h1.1.1.1 h2.1.1.1
    let expression := -gaussianSigma kappa sigma1 sigma1 0 +
      gaussianSigma kappa sigma1 sigma2 (u2 - u1)
    Summable (gibbsSeriesTerm kappa sigma1) ∧
    Summable (gibbsSeriesTerm kappa sigma2) ∧
    D < ⊤ ∧ 0 ≤ expression ∧ D.toReal = expression := 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 Eq. (A20): general-mean Gaussian relative entropy on its finite Gibbs domain

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$ assigns unitary bounded operators to real vectors $\xi\in\mathbb R^J$ , 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$ , bounded complex linear operators $\rho_1,\rho_2$ on $\mathcal H_n$ , real vectors $u_1,u_2\in\mathbb R^J$ , and real $J\times J$ matrices $\sigma_1,\sigma_2$ be given. For each $r=1,2$ , assume a representation $\rho_rx=\sum_\ell\langle v_\ell,x\rangle w_\ell$ with $\sum_\ell\|v_\ell\|\|w_\ell\|<\infty$ , self-adjointness and nonnegative quadratic forms for $\rho_r$ , a summable number-basis trace equal to $1$ , and summability of $\sum_j(\sum_mj_m)\operatorname{Re}\langle e_j,\rho_re_j\rangle$ . Define $\Omega_{(m,0),(m,1)}=1$ , $\Omega_{(m,1),(m,0)}=-1$ , with other entries zero. Assume $2\kappa\sigma_r$ is symmetric and positive definite, $2\kappa\sigma_r+i\Omega$ is positive semidefinite, and every trace series of $\rho_rW(\xi)$ is summable with

\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).

Also assume, for both $r$ , that $\sigma_r$ is symmetric and positive definite and that $\kappa\sigma_r+\frac{i}{2}\Omega$ is positive definite. Set

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

where the real part is entrywise, and define, for real matrices $\alpha,\beta$ and real vector $d$ ,

S(\alpha,\beta,d)= \frac{ \log\!\left(\operatorname{Re}\det(\kappa\beta+\tfrac{i}{2}\Omega)\right) +\kappa\operatorname{tr}(\alpha G_\kappa(\beta)) +\kappa\sum_{a,b}d_aG_\kappa(\beta)_{ab}d_b }{2\log2}, \quad G_\kappa(\beta)= \operatorname{Re}\!\left[ 2i\Omega\sum_{k=0}^{\infty} \frac{\bigl((2\kappa\beta(i\Omega))^{-1}\bigr)^{2k+1}}{2k+1} \right].

For each finite orthonormal family $v_0,\ldots,v_{m-1}$ in $\mathcal H_n$ , form $X_{ab}=\langle v_a,\rho_1v_b\rangle$ , $Y_{ab}=\langle v_a,\rho_2v_b\rangle$ , and give this pair the value $+\infty$ if $\ker Y\not\subseteq\ker X$ , and otherwise the value $\max\{0,\operatorname{Re}\operatorname{tr}(h(X)-X\log(Y)-X+Y)\}$ , where $h(x)=x\log x$ and both matrix functions use the real continuous functional calculus. Let $D\in[0,\infty]$ be the supremum of these values over all natural numbers $m$ and all such families, divided by $\log2$ . Then

\sum_kH_{1,k}\ \text{and}\ \sum_kH_{2,k}\ \text{are summable},\qquad D<+\infty,\qquad 0\le -S(\sigma_1,\sigma_1,0)+S(\sigma_1,\sigma_2,u_2-u_1),

and

D_{\mathrm{real}} =-S(\sigma_1,\sigma_1,0)+S(\sigma_1,\sigma_2,u_2-u_1),

where $D_{\mathrm{real}}$ is the real conversion of the now-finite extended nonnegative value $D$ . Empty orthonormal families and $n=0$ are 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