Expectation-value QNTK is symmetric and positive semidefinite

Proved

QAlgorithms.Papers.Independent.Intakenext100.P88.expectation_kernel_psd

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

The circuit acts on a nonzero finite-dimensional complex Hilbert space $H=\mathbb C^h$ and has the ordered form $U(\theta)=\prod_{\ell=1}^L W_\ell\exp(i\theta_\ell X_\ell)$ , with fixed unitary $W_\ell$ , Hermitian $X_\ell$ , and real angles. Products are written in increasing index order and the rightmost factor acts first. Feature vectors $\phi(x)$ have norm one. For Hermitian observables $O_i$ , put $z_{x,i}(\theta)=\langle U(\theta)\phi(x),O_iU(\theta)\phi(x)\rangle\in\mathbb R$ .

For arbitrary angles define $K_{ab}=\sum_\ell\partial_{\theta_\ell}z_a\,\partial_{\theta_\ell}z_b$ , where $a,b$ range over data-observable pairs. Then

K_{ab}=K_{ba},\qquad [K_{a_p a_q}]_{p,q=1}^n\succeq0

for every finite list $a_1,\ldots,a_n$ , including an empty list. Thus an infinite data space is handled through its finite Gram submatrices. No entrywise positivity or nonsingularity is claimed. This supplies a positive semidefinite kernel for the expectation model.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P88

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakenext100.P88

open scoped BigOperators ComplexConjugate Topology NNReal ComplexOrder

open MeasureTheory ProbabilityTheory Filter

/-- PDF p.24 SM Theorem 1, Eq.(94): symmetry and PSD for every finite Gram submatrix.
No finite-dimensional operator on an infinite data space is postulated. -/
theorem expectation_kernel_psd {D I : Type*} [Fintype I] {h L : ℕ}
    (M : ExpectationNetwork D I h L) (theta : Fin L → ℝ) :
    (∀ a b, expectationKernel M theta a b = expectationKernel M theta b a) ∧
    ∀ (n : ℕ) (a : Fin n → D × I),
      Matrix.PosSemidef (fun i j => expectationKernel M theta (a i) (a j)) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P88

end

Source

Representation Learning via Quantum Neural Tangent Kernels, arXiv:2111.04225v3, PDF p. 24, SM Theorem 1; Eq.(94)

Read-back

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

For arbitrary types $D,I$ , with $I$ finite, natural numbers $h,L$ , every model $M$ described below, and every real parameter vector $\theta=(\theta_l)_{0\le l<L}$ , a kernel is symmetric and all its finite sampled matrices are positive semidefinite. The model supplies $h>0$ , unitary complex $h\times h$ matrices $W_l$ , Hermitian complex $h\times h$ matrices $X_l$ , unit vectors $\phi_x\in\mathbb C^h$ for all $x\in D$ , and Hermitian matrices $O_i$ for all $i\in I$ . Define

U(\eta)=\prod_{l=0}^{L-1}W_l\exp(i\eta_lX_l), \qquad f_{x,i}(\eta)=\operatorname{Re}\langle U(\eta)\phi_x,\,O_iU(\eta)\phi_x\rangle,

with increasing product order, identity empty product, and standard matrix action and complex Euclidean inner product. For $a=(x,i)\in D\times I$ , let

d_{a,l}(\theta)= \left.\frac{d}{ds}\, f_{x,i}\!\left(\operatorname{update}(\theta,l,s)\right)\right|_{s=\theta_l}, \qquad K_\theta(a,b)=\sum_{l=0}^{L-1}d_{a,l}(\theta)d_{b,l}(\theta),

where the update changes only coordinate $l$ , and derivatives are the total real one-variable derivative operation, assigned zero when differentiability fails. The asserted conjunction is that $K_\theta(a,b)=K_\theta(b,a)$ for every $a,b\in D\times I$ , and that for every natural number $n$ and every function $a:\{0,\ldots,n-1\}\to D\times I$ , the real matrix $G_{pq}=K_\theta(a(p),a(q))$ is symmetric and satisfies

\forall\,c\in\mathbb R^n,\qquad \sum_{p=0}^{n-1}\sum_{q=0}^{n-1}c_p\,K_\theta(a(p),a(q))\,c_q\ge0.

The sampled points may repeat. The case $n=0$ is included, as is $L=0$ , when the kernel is zero. Either $D$ or $I$ may be empty, making the pointwise symmetry assertion vacuous and leaving no sampling functions for positive $n$ ; $D$ need not be finite.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph