Quantum kernel methods: the fidelity kernel and its Gram-matrix positive semidefiniteness

A data-encoding quantum feature map sends a classical input x to a quantum state |φ(x)⟩. The induced fidelity quantum kernel is k(x, y) = |⟨φ(x) | φ(y)⟩|² (for pure states this equals tr[ρ(x) ρ(y)], the Hilbert–Schmidt inner product of the density operators). The core fact that makes such a k a legitimate kernel for classical kernel methods (SVMs, etc.) is that every Gram matrix K_{ij} = k(xᵢ, xⱼ) is positive semidefinite.

The proof realizes the fidelity kernel as a genuine inner-product Gram matrix: with the feature vector w(x) := φ(x) ⊗ conj φ(x) one has ⟨w(x), w(y)⟩ = ⟨φ(x), φ(y)⟩ · conj⟨φ(x), φ(y)⟩ = |⟨φ(x), φ(y)⟩|² (via PureState.inner_tensor_tensor), so the kernel Gram matrix factors as K = Bᴴ B and is positive semidefinite by Matrix.posSemidef_conjTranspose_mul_self.

Sources: Schuld & Killoran (2019), Quantum machine learning in feature Hilbert spaces; Schuld (2021), Supervised quantum machine learning models are kernel methods.

Main definitions / results

• LeanPool.LeanQuantumAlg.PureState.conjState — elementwise complex conjugate of a state.
• LeanPool.LeanQuantumAlg.quantumKernel — the fidelity quantum kernel |⟨φ(x), φ(y)⟩|².
• LeanPool.LeanQuantumAlg.quantumKernel_eq_inner_featureTensor — the kernel as an inner product of feature vectors φ(x) ⊗ conj φ(x).
• LeanPool.LeanQuantumAlg.quantumKernel_gram_posSemidef — the kernel Gram matrix is positive semidefinite (the validity-of-the-kernel theorem). Being positive semidefinite it is in particular Hermitian, i.e. symmetric.
• LeanPool.LeanQuantumAlg.quantumKernel_self — the diagonal value on a pure state.

noncomputable def QuantumAlg.PureState.conjState {n : ℕ} (ψ : PureState n) : PureState n

Elementwise complex conjugate of a pure state.

Equations

• ψ.conjState = QuantumAlg.PureState.ofVec (WithLp.toLp 2 fun (i : Fin (2 ^ n)) => (starRingEnd ℂ) (ψ.vec.ofLp i)) ⋯

@[simp]

theorem QuantumAlg.PureState.conjState_apply {n : ℕ} (ψ : PureState n) (i : Fin (2 ^ n)) : ψ.conjState.vec.ofLp i = (starRingEnd ℂ) (ψ.vec.ofLp i)

theorem QuantumAlg.PureState.inner_conjState {n : ℕ} (a b : PureState n) : inner ℂ a.conjState b.conjState = (starRingEnd ℂ) (inner ℂ a b)

Conjugating both arguments conjugates the inner product.

noncomputable def QuantumAlg.featureTensor {n : ℕ} {X : Type u_1} (φ : X → PureState n) (x : X) : PureState (n + n)

The feature vector φ(x) ⊗ conj φ(x) whose inner products realize the fidelity kernel as a Gram matrix.

Equations

• QuantumAlg.featureTensor φ x = (φ x).tensor (φ x).conjState

noncomputable def QuantumAlg.quantumKernel {n : ℕ} {X : Type u_1} (φ : X → PureState n) (x y : X) : ℂ

The fidelity quantum kernel k(x, y) = |⟨φ(x), φ(y)⟩|², written as the complex product ⟨φ(x), φ(y)⟩ · conj⟨φ(x), φ(y)⟩ (a nonnegative real).

Equations

• QuantumAlg.quantumKernel φ x y = inner ℂ (φ x) (φ y) * (starRingEnd ℂ) (inner ℂ (φ x) (φ y))

theorem QuantumAlg.quantumKernel_eq_inner_featureTensor {n : ℕ} {X : Type u_1} (φ : X → PureState n) (x y : X) : quantumKernel φ x y = inner ℂ (featureTensor φ x) (featureTensor φ y)

The fidelity kernel is the inner product of the feature vectors φ(·) ⊗ conj φ(·).

theorem QuantumAlg.quantumKernel_self {n : ℕ} {X : Type u_1} (φ : X → PureState n) (x : X) : quantumKernel φ x x = 1

The diagonal kernel value is 1.

theorem QuantumAlg.quantumKernel_gram_posSemidef {n : ℕ} {X : Type u_1} {ι : Type u_2} [Finite ι] (φ : X → PureState n) (x : ι → X) : (Matrix.of fun (i j : ι) => quantumKernel φ (x i) (x j)).PosSemidef

Validity of the quantum kernel. For any finite family of inputs, the fidelity-kernel Gram matrix K_{ij} = k(xᵢ, xⱼ) is positive semidefinite, hence k is a legitimate (positive-semidefinite) kernel.

theorem QuantumAlg.QuantumKernel.main {n : ℕ} {X : Type u_1} {ι : Type u_2} [Finite ι] (φ : X → PureState n) (x : ι → X) : (Matrix.of fun (i j : ι) => quantumKernel φ (x i) (x j)).PosSemidef

Main theorem: fidelity quantum-kernel Gram matrices are positive semidefinite.

theorem QuantumAlg.QuantumKernel.main_feature_tensor {n : ℕ} {X : Type u_1} (φ : X → PureState n) (x y : X) : quantumKernel φ x y = inner ℂ (featureTensor φ x) (featureTensor φ y)

Public supporting theorem: the fidelity kernel is an inner product after tensor lifting.

theorem QuantumAlg.QuantumKernel.main_self {n : ℕ} {X : Type u_1} (φ : X → PureState n) (x : X) : quantumKernel φ x x = 1

Public supporting theorem: the diagonal fidelity-kernel value of a pure state is one.