Gaussian quadratic mean, second moment, and variance

Open

QAlgorithms.Papers.Independent.Intakethird100.P17.gaussian_quadratic_moments

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

prove2quantum

Let $n\ge0$ and $\kappa>0$ . On the full $n$ -mode oscillator space, let $\rho$ be a normalized, centered, finite-energy Gaussian density with centered half-anticommutator covariance $\sigma$ . Write $q=(x_1,p_1,\ldots,x_n,p_n)^T$ , with $[q,q^T]=i\Omega/\kappa$ and $\Omega=\bigoplus_{j=1}^n\left(\begin{smallmatrix}0&1\\-1&0\end{smallmatrix}\right)$ . For every real symmetric $2n\times2n$ matrix $A$ , set $Q=q^TAq$ . The polynomial products and density-weighted traces converge, and

\begin{aligned} \mathbb E_\rho Q&=\operatorname{tr}(\sigma A),\\ \mathbb E_\rho Q^2&=\operatorname{tr}(\sigma A)^2+2\operatorname{tr}(A\sigma A\sigma)-\frac{\operatorname{tr}(A\Omega A\Omega^T)}{2\kappa^2},\\ \operatorname{Var}_\rho Q&=2\operatorname{tr}(A\sigma A\sigma)+\frac{\operatorname{tr}(A\Omega A\Omega)}{2\kappa^2}. \end{aligned}

These identities include pure Gaussian states and provide the quadratic moments needed for the entropy-variance calculation.

Formalization Note The observables use their actual creation/annihilation coefficients on the full finite-particle core. Absolute convergence of the infinite pairings is a conclusion, rather than an assumed moment identity.

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, (A8),(A11),(A12).
Real symmetric A and actual centered normalized Gaussian densities, including
pure states. All polynomial traces and core products converge. -/
theorem gaussian_quadratic_moments {n : ℕ}
    (W : FockWeylSystem n) (kappa : ℝ) (hkappa : 0 < kappa)
    (rho : ModeOperator n) (sigma A : Matrix (Quadrature n) (Quadrature n) ℝ)
    (hrho : GaussianInConvention W kappa rho 0 sigma) (hA : A.transpose = A) :
    let Q := quadraticKernel kappa A
    let Omega := canonicalOmega n
    (∀ a b : Quadrature n, PolynomialProductSummable (quadratureKernel kappa a) (quadratureKernel kappa b)) ∧
    PolynomialProductSummable Q Q ∧
    PolynomialPairingSummable rho Q ∧
    PolynomialPairingSummable rho (polynomialKernelProduct Q Q) ∧
    polynomialExpectation rho Q = (sigma * A).trace ∧
    polynomialExpectation rho (polynomialKernelProduct Q Q) =
      (sigma * A).trace ^ 2 + 2 * (A * sigma * A * sigma).trace -
        (A * Omega * A * Omega.transpose).trace / (2 * kappa ^ 2) ∧
    quadraticVariance rho kappa A = 2 * (A * sigma * A * sigma).trace +
      (A * Omega * A * Omega).trace / (2 * kappa ^ 2) := 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. (A8),(A11),(A12): Gaussian quadratic moments

Read-back

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

For every natural number $n$ , put $\mathcal H_n=\ell^2(F;\mathbb C)$ , where $F=\{0,\ldots,n-1\}\to\mathbb N$ , let $e_j$ be its standard basis, and put $J=\{0,\ldots,n-1\}\times\{0,1\}$ . Suppose $W$ assigns to each real vector $\xi\in\mathbb R^J$ a unitary bounded operator whose matrix entries are

(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$ be a bounded complex linear operator on $\mathcal H_n$ , and let $\sigma,A$ be real $J\times J$ matrices with $A^{\mathsf T}=A$ . Assume that $\rho x=\sum_r\langle v_r,x\rangle u_r$ for some sequences satisfying $\sum_r\|u_r\|\|v_r\|<\infty$ , that $\rho^*=\rho$ and $\operatorname{Re}\langle x,\rho x\rangle\ge0$ for every $x$ , that $\sum_j\langle e_j,\rho e_j\rangle$ is summable and equals $1$ , and that $\sum_j(\sum_rj_r)\operatorname{Re}\langle e_j,\rho e_j\rangle$ is summable. Write $\Omega_{(r,0),(r,1)}=1$ , $\Omega_{(r,1),(r,0)}=-1$ , with all other entries zero. Also assume that $2\kappa\sigma$ is symmetric and positive definite, that $2\kappa\sigma+i\Omega$ is positive semidefinite, and that for every real $\xi$ , the trace series of $\rho W(\xi)$ is summable and

\sum_j\langle e_j,\rho W(\xi)e_j\rangle =\exp\!\left(-\kappa\sum_{a,b\in J}\xi_a\sigma_{ab}\xi_b\right).

For $a=(r,t)\in J$ , define

R_r(i,j)= \begin{cases}\sqrt{j_r+1},&i=j[r\mapsto j_r+1],\\0,&\text{otherwise},\end{cases} \quad q_{(r,0)}(i,j)=\frac{R_r(i,j)+R_r(j,i)}{\sqrt{2\kappa}}, \quad q_{(r,1)}(i,j)= \frac{i\bigl(R_r(i,j)-R_r(j,i)\bigr)}{\sqrt{2\kappa}},

and, for kernels $K,L$ , set $(K\star L)_{ij}=\sum_{\ell\in F}K_{i\ell}L_{\ell j}$ , $Q_{ij}=\sum_{a,b\in J}A_{ab}(q_a\star q_b)_{ij}$ , and

E_\rho(K)=\operatorname{Re}\sum_{i,j\in F}(\rho e_j)_iK_{ji}.

Then every series defining $(q_a\star q_b)_{ij}$ , for every $a,b,i,j$ , and every series defining $(Q\star Q)_{ij}$ , is summable; the jointly indexed pairing series defining $E_\rho(Q)$ and $E_\rho(Q\star Q)$ are also summable; and

E_\rho(Q)=\operatorname{tr}(\sigma A),

E_\rho(Q\star Q) =\operatorname{tr}(\sigma A)^2 +2\operatorname{tr}(A\sigma A\sigma) -\frac{\operatorname{tr}(A\Omega A\Omega^{\mathsf T})}{2\kappa^2}, \qquad E_\rho(Q\star Q)-E_\rho(Q)^2 =2\operatorname{tr}(A\sigma A\sigma) +\frac{\operatorname{tr}(A\Omega A\Omega)}{2\kappa^2}.

There is no assumption $n>0$ ; at $n=0$ , the quadrature index set is empty and these expectations and variance are zero.

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