Embedding quantum kernels: density-matrix realization (expressivity)

The genuine core of Gil-Fuster, Eisert, Dunjko (2023) Theorem 1: every feature-map kernel is realizable, up to a positive affine transform, by valid density matrices via the embedding quantum kernel tr{ρ(x)ρ(x')}. Converse of quantumKernel_gram_posSemidef. No assumptions.

noncomputable def QuantumAlg.offDiagEmb {r : ℕ} (v : Fin r → ℂ) : Matrix (Fin 1 ⊕ Fin r) (Fin 1 ⊕ Fin r) ℂ

Off-diagonal Hermitian embedding of a feature vector v into Fin 1 ⊕ Fin r.

Equations

• QuantumAlg.offDiagEmb v = Matrix.fromBlocks 0 (Matrix.of fun (x : Fin 1) (k : Fin r) => v k) (Matrix.of fun (k : Fin r) (x : Fin 1) => (starRingEnd ℂ) (v k)) 0

theorem QuantumAlg.trace_fromBlocks' {r : ℕ} {A : Matrix (Fin 1) (Fin 1) ℂ} {B : Matrix (Fin 1) (Fin r) ℂ} {C : Matrix (Fin r) (Fin 1) ℂ} {D : Matrix (Fin r) (Fin r) ℂ} : (Matrix.fromBlocks A B C D).trace = A.trace + D.trace

A local trace-of-block-matrix helper (trace_fromBlocks is not in Mathlib).

theorem QuantumAlg.offDiagEmb_isHermitian {r : ℕ} (v : Fin r → ℂ) : (offDiagEmb v).IsHermitian

theorem QuantumAlg.offDiagEmb_trace_zero {r : ℕ} (v : Fin r → ℂ) : (offDiagEmb v).trace = 0

theorem QuantumAlg.trace_offDiagEmb_mul {r : ℕ} (v w : Fin r → ℂ) : (offDiagEmb v * offDiagEmb w).trace = 2 * ↑(∑ k : Fin r, (starRingEnd ℂ) (v k) * w k).re

The HS inner product of two off-diagonal embeddings: tr(offDiagEmb v * offDiagEmb w) = 2·Re⟨v,w⟩ (a real number).

theorem QuantumAlg.one_add_offDiagEmb_eq {r : ℕ} (v : Fin r → ℂ) : 1 + offDiagEmb v = Matrix.fromBlocks 1 (Matrix.of fun (x : Fin 1) (k : Fin r) => v k) (Matrix.of fun (k : Fin r) (x : Fin 1) => (starRingEnd ℂ) (v k)) 1

1 + offDiagEmb v written as a bordered block matrix.

theorem QuantumAlg.one_add_offDiagEmb_posSemidef {r : ℕ} (v : Fin r → ℂ) (hv : ∑ k : Fin r, Complex.normSq (v k) ≤ 1) : (1 + offDiagEmb v).PosSemidef

Validity crux: 1 + offDiagEmb v is positive semidefinite when ∑ ‖v k‖² ≤ 1. Proved by the fromBlocks₂₂ Schur complement, which collapses to the 1×1 matrix [1 - ∑ normSq (v k)].

noncomputable def QuantumAlg.densityOf {r : ℕ} (v : Fin r → ℂ) : Matrix (Fin 1 ⊕ Fin r) (Fin 1 ⊕ Fin r) ℂ

The maximally-mixed-plus-perturbation density operator for feature vector v.

Equations

• QuantumAlg.densityOf v = (↑r + 1)⁻¹ • (1 + QuantumAlg.offDiagEmb v)

theorem QuantumAlg.densityOf_posSemidef {r : ℕ} (v : Fin r → ℂ) (hv : ∑ k : Fin r, Complex.normSq (v k) ≤ 1) : (densityOf v).PosSemidef

theorem QuantumAlg.densityOf_isHermitian {r : ℕ} (v : Fin r → ℂ) (hv : ∑ k : Fin r, Complex.normSq (v k) ≤ 1) : (densityOf v).IsHermitian

theorem QuantumAlg.densityOf_trace_one {r : ℕ} (v : Fin r → ℂ) : (densityOf v).trace = 1

theorem QuantumAlg.densityOf_mul_trace {r : ℕ} (v w : Fin r → ℂ) : (densityOf v * densityOf w).trace = (↑↑r + 1)⁻¹ ^ 2 * (↑(1 + r) + 2 * ↑(∑ k : Fin r, (starRingEnd ℂ) (v k) * w k).re)

EQK trace identity: the embedding quantum kernel of two feature vectors is a positive affine image of Re⟨v,w⟩ (here in the raw form c²·(D + 2·Re⟨v,w⟩), c = 1/D, D = r+1).

theorem QuantumAlg.eqk_realizes {r : ℕ} {ι : Type u_1} (φ : ι → Fin r → ℂ) (hφ : ∀ (i : ι), ∑ k : Fin r, Complex.normSq (φ i k) ≤ 1) : (∀ (i : ι), (densityOf (φ i)).IsHermitian ∧ (densityOf (φ i)).trace = 1 ∧ (densityOf (φ i)).PosSemidef) ∧ ∀ (i j : ι), (densityOf (φ i) * densityOf (φ j)).trace = (↑↑r + 1)⁻¹ ^ 2 * (↑(1 + r) + 2 * ↑(∑ k : Fin r, (starRingEnd ℂ) (φ i k) * φ j k).re)

Approximate universality (finite, positive-affine form), Gil-Fuster 2023 Thm 1. Any normalized feature map φ is realized by a family of genuine density matrices whose embedding quantum kernel equals c²·(D + 2·Re⟨φ_i,φ_j⟩) — a positive affine image of the feature kernel Re⟨φ_i,φ_j⟩ (exact for real feature maps).

theorem QuantumAlg.eqk_nonempty : ∃ (r : ℕ) (φ : Fin 2 → Fin r → ℂ), (∀ (i : Fin 2), (densityOf (φ i)).PosSemidef ∧ (densityOf (φ i)).trace = 1) ∧ (densityOf (φ 0) * densityOf (φ 0)).trace ≠ (densityOf (φ 0) * densityOf (φ 1)).trace

Non-vacuity: a concrete two-input feature map gives valid density matrices realizing a non-constant embedding quantum kernel.