Gaussian relative entropy variance

Open

QAlgorithms.Papers.Independent.Intakethird100.P17.gaussian_relative_entropy_variance

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. The centered half-anticommutator covariance convention is $[q,q^T]=i\Omega/\kappa$ , with canonical interleaved $\Omega$ . Assume every symplectic eigenvalue of each covariance exceeds $1/(2\kappa)$ ; both finite mean vectors are arbitrary. Write $G_j=2i\Omega\operatorname{arcoth}(2\kappa\sigma_j i\Omega)$ , $\widetilde G=G_1-G_2$ , $\delta=u_1-u_2$ , $B=8\kappa^2G_2\sigma_1G_2$ , and $S=S(\rho_1\Vert\rho_2)$ in bits. Then $S$ and the centered operator log-likelihood variance are finite, and

\begin{aligned} V(\rho_1\Vert\rho_2) &:=\operatorname{Tr}\!\left[\rho_1(\log_2\rho_1-\log_2\rho_2-S)^2\right]\\ &=\frac{4\kappa^2\operatorname{tr}(\sigma_1\widetilde G\sigma_1\widetilde G)+\operatorname{tr}(\widetilde G\Omega\widetilde G\Omega)+\delta^TB\delta}{2(2\ln2)^2}. \end{aligned}

The positive sign before the term containing two copies of $\Omega$ is part of the formula. The variance vanishes for identical states.

Formalization Note The left side is the convergent density-weighted limit of the square of the actual centered operator log difference. The order of multiplication is retained; this is not a classical variance that assumes the operators commute.

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.8, final unnumbered formula.
Variance of the actual centered NONCOMMUTATIVE operator log difference.
Both covariances have finite Gibbs matrices; all means are allowed. -/
theorem gaussian_relative_entropy_variance {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 := gaussianVarianceExpression kappa sigma1 sigma2 (u1 - u2)
    Summable (gibbsSeriesTerm kappa sigma1) ∧
    Summable (gibbsSeriesTerm kappa sigma2) ∧ D < ⊤ ∧
    (∀ k, let L := oscillatorLogCutoff rho1 k - oscillatorLogCutoff rho2 k -
        (D.toReal : ℂ) • (1 : ModeOperator n)
      TraceSummable (rho1.comp (L.comp L))) ∧
    Tendsto (relativeVarianceCutoff rho1 rho2 D.toReal) atTop (nhds expression) ∧
    oscillatorRelativeVariance rho1 rho2 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. 8, Appendix A final unnumbered formula: relative entropy variance

Read-back

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

Let $n$ be any natural number, including $0$ , let $\mathcal H=\ell^2(\mathbb N^n;\mathbb C)$ , and write $|j\rangle$ for its standard basis vector indexed by $j\in\mathbb N^n$ . All operators below are bounded complex-linear operators on $\mathcal H$ , and their specified trace is $\operatorname{tr}T=\sum_j\langle j|T|j\rangle$ ; “trace summable” means that this complex diagonal series is summable. Here an operator $T$ is called trace class precisely when there are sequences $a_r,b_r\in\mathcal H$ with $\sum_r\|a_r\|\|b_r\|<\infty$ and $Tx=\sum_r\langle b_r,x\rangle a_r$ for every $x\in\mathcal H$ ; positivity means $T^*=T$ and $\operatorname{Re}\langle x,Tx\rangle\ge0$ for every $x$ . Index phase coordinates by $(k,a)\in\{0,\ldots,n-1\}\times\{0,1\}$ , and let $\Omega$ have entries $\Omega_{(k,0),(k,1)}=1$ , $\Omega_{(k,1),(k,0)}=-1$ , and all other entries zero. Fix a system $W$ assigning a unitary operator $W(\xi)$ to every real phase vector $\xi$ , with number-basis coefficients

[W(\xi)]_{ij}=\prod_{k=0}^{n-1}d_{i_kj_k}(-\xi_{k,1}+\mathrm i\xi_{k,0}),\qquad d_{ab}(z)=e^{-|z|^2/2}\sqrt{a!\,b!} \sum_{r=0}^{\min(a,b)} \frac{z^{a-r}(-\overline z)^{b-r}}{r!(a-r)!(b-r)!}.

For every real $\kappa>0$ , every pair of operators $\rho_1,\rho_2$ , real phase vectors $u_1,u_2$ , and real phase-coordinate matrices $\sigma_1,\sigma_2$ , assume, for each $i=1,2$ , that $\rho_i$ is positive and trace class, is trace summable with trace $1$ , and satisfies the finite-energy summability condition

\sum_{j\in\mathbb N^n}\left(\sum_{m=0}^{n-1}j_m\right) \operatorname{Re}\langle j|\rho_i|j\rangle<\infty.

Assume also that $2\kappa\sigma_i$ is symmetric and positive definite, that $2\kappa\sigma_i+\mathrm i\Omega$ is positive semidefinite, and that, for every real phase vector $\xi$ , $\rho_iW(\xi)$ is trace summable and

\operatorname{tr}(\rho_iW(\xi)) =\exp\!\left(-\kappa\,\xi^{\mathsf T}\sigma_i\xi +\mathrm i\sqrt{2\kappa}\,u_i^{\mathsf T}\xi\right).

The further strict covariance hypotheses require $\sigma_i^{\mathsf T}=\sigma_i$ , $\sigma_i$ positive definite, and $\kappa\sigma_i+\frac{\mathrm i}{2}\Omega$ positive definite as a complex matrix. Define $D\in[0,\infty]$ as follows: for every $m\in\mathbb N$ and every orthonormal family $v_0,\ldots,v_{m-1}\in\mathcal H$ , form the compressed matrices $X_{ab}=\langle v_a,\rho_1v_b\rangle$ and $Y_{ab}=\langle v_a,\rho_2v_b\rangle$ ; assign this pair the value

\mathcal R(X,Y)= \begin{cases} \max\!\left\{0,\operatorname{Re}\operatorname{Tr} \bigl(f(X)-X\log Y-X+Y\bigr)\right\}, &\ker Y\subseteq\ker X,\\ +\infty,&\text{otherwise}, \end{cases} \qquad f(x)=x\log x, \quad D=\frac{\sup_{m,v}\mathcal R(X,Y)}{\log2}.

The matrix functions here use continuous functional calculus and the total real logarithm, for which $\log0=0$ ; the supremum includes the empty orthonormal family $m=0$ . Regarding real matrices as complex matrices when needed, define

B_i=2\kappa\,\sigma_i(\mathrm i\Omega),\qquad T_{i,r}=\frac{(B_i^{-1})^{2r+1}}{2r+1},\qquad G_i=\operatorname{Re}\!\left(2\mathrm i\,\Omega\sum_{r=0}^{\infty}T_{i,r}\right),

where the real part is taken entrywise and matrix inverses are the total matrix inverse, equal to zero for a singular matrix. Put $\delta=u_1-u_2$ , $\Delta G=G_1-G_2$ , and

V= \frac{ 4\kappa^2\operatorname{Tr}(\sigma_1\Delta G\,\sigma_1\Delta G) +\operatorname{Tr}(\Delta G\,\Omega\Delta G\,\Omega) +\delta^{\mathsf T}(8\kappa^2G_2\sigma_1G_2)\delta }{ 2(2\log2)^2 }.

For $k\in\mathbb N$ , let

\ell_k(\rho)= \left[x\longmapsto\frac{\log\max\{x,1/(k+1)\}}{\log2}\right](\rho), \qquad L_k=\ell_k(\rho_1)-\ell_k(\rho_2)-D_{\mathbb R}I,

using continuous functional calculus, where $D_{\mathbb R}$ is the real-value conversion of $D$ (this conversion sends $+\infty$ to zero). Then both matrix series $\sum_rT_{1,r}$ and $\sum_rT_{2,r}$ are summable, $D<+\infty$ , every operator $\rho_1L_k^2$ is trace summable, and

\lim_{k\to\infty}\operatorname{Re}\operatorname{tr}(\rho_1L_k^2)=V.

Moreover, the quantity defined by applying the general filter-limit operator to this same sequence, namely the specified oscillator relative variance with mean $D_{\mathbb R}$ , equals $V$ . No positive-mode hypothesis is imposed: $n=0$ is included, with empty phase-coordinate matrices and empty phase-coordinate sums.

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