Positive definiteness of an exponential hermitian kernel

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.exponential_kernel_criterion

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

prove2quantum

Let $V$ be a vector space over $\mathbb K=\mathbb R$ or $\mathbb C$ , and let $\beta:V\times V\to\mathbb K$ be a hermitian form, with the first argument linear; in the real case this means symmetric bilinear. Then

\bigl[(v,w)\mapsto e^{\beta(v,w)}\bigr]\text{ is positive definite}\quad\Longleftrightarrow\quad\beta(v,v)\geq0\text{ for every }v\in V.

Positive definiteness means that every finite Gram sum is a real nonnegative scalar. Degenerate forms and the zero vector space are included.

This criterion relates hermitian forms to exponential kernels. The scalar type RCLike uniformly covers both real and complex cases; positivity is not assumed to define the exponential.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P92

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P92

open scoped ComplexConjugate BigOperators NNReal ENNReal

open MeasureTheory

attribute [local instance] Classical.propDecidable

universe u v

variable (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]

variable {E}

/-- Lemma C.5, PDF p. 52, simultaneously for real and complex vector spaces
(`RCLike`). The zero vector space and degenerate hermitian forms are included. -/
theorem exponential_kernel_criterion (K : Type*) [RCLike K]
    (V : Type v) [AddCommGroup V] [Module K V] (beta : V → V → K)
    (hBeta : IsHermitianForm K beta) :
    IsPositiveKernel K (fun x y => NormedSpace.exp (beta x y)) ↔
      ∀ x, ∃ a : ℝ, 0 ≤ a ∧ beta x x = (a : K) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, PDF p. 52, Lemma C.5

Read-back

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

Let $K$ be a real-or-complex scalar field with an $\mathrm{RCLike}$ structure, let $V$ be an additive commutative group and a $K$ -module, and let $\beta:V\times V\to K$ . Assume that, for all $x,y,z\in V$ and $a\in K$ ,

\begin{gathered} \beta(x+y,z)=\beta(x,z)+\beta(y,z),\qquad \beta(ax,y)=a\beta(x,y),\\ \beta(x,y+z)=\beta(x,y)+\beta(x,z),\qquad \beta(x,ay)=\overline a\,\beta(x,y),\qquad \overline{\beta(x,y)}=\beta(y,x). \end{gathered}

Then the following are equivalent: for every natural number $n$ , every family $x_1,\ldots,x_n\in V$ , and every family $c_1,\ldots,c_n\in K$ , there is a real number $a\geq0$ such that

\sum_{i=1}^{n}\sum_{j=1}^{n} \overline{c_i}\,\exp\!\bigl(\beta(x_i,x_j)\bigr)c_j=a \quad\text{in }K;

and, for every $x\in V$ , there is a real number $a\geq0$ such that $\beta(x,x)=a$ in $K$ . Here conjugation means the scalar star operation, and real numbers are embedded into $K$ . The first condition includes $n=0$ , when the sum is empty and equals 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