Fourier representation of the quantum kernel

For an N-input data-encoding circuit with a common diagonal generator, the fidelity quantum kernel κ(x, x') = |⟨φ(x')|φ(x)⟩|² is a finite sum of characters e^{i⟨s,x⟩} e^{i⟨t,x'⟩} whose frequencies are differences of the generator's eigenvalues (Schuld 2021). The encoding gates are modelled directly as diagonal phase matrices — the standard WLOG-diagonalization step — so the Fourier structure is proved genuinely while avoiding the matrix exponential.

The proof shows each component of the feature state is an TrigPolynomial (by closure under applying a constant matrix and a diagonal phase gate), hence the overlap and its squared modulus are TrigPolynomials; collecting by frequency gives the representation.

noncomputable def QuantumAlg.diagPhaseGate {d : ℕ} (lam : Fin d → ℝ) (xk : ℝ) : Matrix (Fin d) (Fin d) ℂ

The diagonal data-encoding phase gate for input coordinate k: diagonal (μ ↦ exp(-i x_k λ_μ)).

Equations

• QuantumAlg.diagPhaseGate lam xk = Matrix.diagonal fun (μ : Fin d) => Complex.exp (-Complex.I * ↑(xk * lam μ))

def QuantumAlg.IsTrigPolynomialVec {N d : ℕ} (v : (Fin N → ℝ) → Fin d → ℂ) : Prop

A data-parametrized vector each of whose components is an trigonometric polynomial.

Equations

• QuantumAlg.IsTrigPolynomialVec v = ∀ (m : Fin d), ∃ (f : QuantumAlg.TrigPolynomial N), ∀ (x : Fin N → ℝ), v x m = f.eval x

theorem QuantumAlg.isTrigPolynomialVec_const {N d : ℕ} (w : Fin d → ℂ) : IsTrigPolynomialVec fun (x : Fin N → ℝ) => w

Any constant vector is an trigonometric-polynomial vector (single zero frequency).

theorem QuantumAlg.IsTrigPolynomialVec.constMul {N d : ℕ} {v : (Fin N → ℝ) → Fin d → ℂ} (hv : IsTrigPolynomialVec v) (M : Matrix (Fin d) (Fin d) ℂ) : IsTrigPolynomialVec fun (x : Fin N → ℝ) => M.mulVec (v x)

Left-multiplication by a constant matrix preserves IsTrigPolynomialVec.

theorem QuantumAlg.IsTrigPolynomialVec.phaseMul {N d : ℕ} {v : (Fin N → ℝ) → Fin d → ℂ} (hv : IsTrigPolynomialVec v) (lam : Fin d → ℝ) (k : Fin N) : IsTrigPolynomialVec fun (x : Fin N → ℝ) => (diagPhaseGate lam (x k)).mulVec (v x)

Left-multiplication by a diagonal phase gate preserves IsTrigPolynomialVec.

noncomputable def QuantumAlg.featState {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (j : ℕ) : (Fin N → ℝ) → Fin d → ℂ

The feature state after j encoding layers: start from ψ, apply the constant unitary W 0, then alternately a phase gate for each coordinate and the next W. featState W lam ψ N x is |φ(x)⟩ for the full N-input circuit.

Equations

• One or more equations did not get rendered due to their size.
• QuantumAlg.featState W lam ψ 0 x✝ = (W 0).mulVec ψ

theorem QuantumAlg.isTrigPolynomialVec_featState {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (j : ℕ) : IsTrigPolynomialVec (featState W lam ψ j)

Every layer of the feature state is an trigonometric-polynomial vector.

Constructive feature components (explicit trigonometric polynomials)

noncomputable def QuantumAlg.tpVecConst {N d : ℕ} (w : Fin d → ℂ) : Fin d → TrigPolynomial N

A constant vector of trigonometric polynomials (each component a single zero-frequency term).

Equations

• QuantumAlg.tpVecConst w m = { freqs := {0}, coeff := fun (x : Fin N → ℝ) => w m }

theorem QuantumAlg.tpVecConst_eval {N d : ℕ} (w : Fin d → ℂ) (m : Fin d) (x : Fin N → ℝ) : (tpVecConst w m).eval x = w m

noncomputable def QuantumAlg.tpVecConstMul {N d : ℕ} (M : Matrix (Fin d) (Fin d) ℂ) (V : Fin d → TrigPolynomial N) : Fin d → TrigPolynomial N

Apply a constant matrix to a vector of trigonometric polynomials.

Equations

• QuantumAlg.tpVecConstMul M V m = QuantumAlg.TrigPolynomial.sum Finset.univ fun (j : Fin d) => QuantumAlg.TrigPolynomial.smul (M m j) (V j)

theorem QuantumAlg.tpVecConstMul_eval {N d : ℕ} (M : Matrix (Fin d) (Fin d) ℂ) (V : Fin d → TrigPolynomial N) (m : Fin d) (x : Fin N → ℝ) : (tpVecConstMul M V m).eval x = ∑ j : Fin d, M m j * (V j).eval x

noncomputable def QuantumAlg.tpVecPhase {N d : ℕ} (lam : Fin d → ℝ) (k : Fin N) (V : Fin d → TrigPolynomial N) : Fin d → TrigPolynomial N

Apply a diagonal phase gate (symbolically, a per-component frequency shift).

Equations

• QuantumAlg.tpVecPhase lam k V m = QuantumAlg.TrigPolynomial.expMul (-lam m • Pi.single k 1) (V m)

theorem QuantumAlg.tpVecPhase_eval {N d : ℕ} (lam : Fin d → ℝ) (k : Fin N) (V : Fin d → TrigPolynomial N) (m : Fin d) (x : Fin N → ℝ) : (tpVecPhase lam k V m).eval x = Complex.exp (-Complex.I * ↑(x k * lam m)) * (V m).eval x

noncomputable def QuantumAlg.featCompC {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (j : ℕ) : Fin d → TrigPolynomial N

The constructive feature component after j layers: an explicit Fin d-indexed family of trigonometric polynomials mirroring featState.

Equations

• One or more equations did not get rendered due to their size.
• QuantumAlg.featCompC W lam ψ 0 = QuantumAlg.tpVecConstMul (W 0) (QuantumAlg.tpVecConst ψ)

theorem QuantumAlg.featState_eq_featCompC {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (j : ℕ) (x : Fin N → ℝ) (m : Fin d) : featState W lam ψ j x m = (featCompC W lam ψ j m).eval x

noncomputable def QuantumAlg.featComp {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (m : Fin d) : TrigPolynomial N

The trigonometric-polynomial witness for component m of the full feature state.

Equations

• QuantumAlg.featComp W lam ψ m = QuantumAlg.featCompC W lam ψ N m

theorem QuantumAlg.featComp_eval {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (m : Fin d) (x : Fin N → ℝ) : featState W lam ψ N x m = (featComp W lam ψ m).eval x

Feature-component frequency invariant

theorem QuantumAlg.tpVecConst_freqs {N d : ℕ} (w : Fin d → ℂ) (m : Fin d) : (tpVecConst w m).freqs = {0}

theorem QuantumAlg.tpVecConstMul_freqs {N d : ℕ} (M : Matrix (Fin d) (Fin d) ℂ) (V : Fin d → TrigPolynomial N) (m : Fin d) : (tpVecConstMul M V m).freqs = Finset.univ.biUnion fun (j : Fin d) => (V j).freqs

theorem QuantumAlg.tpVecPhase_freqs {N d : ℕ} (lam : Fin d → ℝ) (k : Fin N) (V : Fin d → TrigPolynomial N) (m : Fin d) : (tpVecPhase lam k V m).freqs = Finset.image (fun (ω : Fin N → ℝ) => ω + -lam m • Pi.single k 1) (V m).freqs

theorem QuantumAlg.featCompC_layer {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (j : ℕ) (m : Fin d) (ω : Fin N → ℝ) : ω ∈ (featCompC W lam ψ j m).freqs → ∀ (a : Fin N), (↑a < j → ∃ (μ : Fin d), ω a = -lam μ) ∧ (j ≤ ↑a → ω a = 0)

After j layers, every feature-component frequency is -λ_μ on coordinates < j and 0 on coordinates ≥ j. Since each input is encoded exactly once, at j = N every coordinate is a negated eigenvalue.

theorem QuantumAlg.featComp_freq {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (m : Fin d) (ω : Fin N → ℝ) (hω : ω ∈ (featComp W lam ψ m).freqs) (a : Fin N) : ∃ (μ : Fin d), ω a = -lam μ

At the full circuit (j = N), every feature-component frequency coordinate is a negated eigenvalue.

noncomputable def QuantumAlg.overlapES {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) : TrigPolynomial (N + N)

The overlap ⟨φ(x')|φ(x)⟩ as a trigonometric polynomial in the concatenated variable.

Equations

• QuantumAlg.overlapES W lam ψ = QuantumAlg.TrigPolynomial.sum Finset.univ fun (m : Fin d) => (QuantumAlg.featComp W lam ψ m).conj.embedR.mul (QuantumAlg.featComp W lam ψ m).embedL

theorem QuantumAlg.overlapES_eval {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (x x' : Fin N → ℝ) : (overlapES W lam ψ).eval (Fin.append x x') = ∑ m : Fin d, (starRingEnd ℂ) (featState W lam ψ N x' m) * featState W lam ψ N x m

noncomputable def QuantumAlg.kernelES {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) : TrigPolynomial (N + N)

The quantum kernel as an trigonometric polynomial: the squared modulus of the overlap.

Equations

• QuantumAlg.kernelES W lam ψ = (QuantumAlg.overlapES W lam ψ).mul (QuantumAlg.overlapES W lam ψ).conj

theorem QuantumAlg.fourier_representation {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (x x' : Fin N → ℝ) : ↑(Complex.normSq (∑ m : Fin d, (starRingEnd ℂ) (featState W lam ψ N x' m) * featState W lam ψ N x m)) = ∑ ω ∈ (kernelES W lam ψ).freqs, (kernelES W lam ψ).coeff ω * Complex.exp (Complex.I * ↑(freqDot ω (Fin.append x x')))

Fourier representation of the quantum kernel (Schuld 2021). The fidelity kernel κ(x,x') = |⟨φ(x')|φ(x)⟩|² is a finite sum of characters e^{i⟨ω,(x,x')⟩} whose frequencies (the elements of (kernelES …).freqs) are differences of the generator's eigenvalue vectors.

theorem QuantumAlg.fourier_real {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (ω : Fin (N + N) → ℝ) : (kernelES W lam ψ).coeffAt ω = (starRingEnd ℂ) ((kernelES W lam ψ).coeffAt (-ω))

Reality condition. The kernel's Fourier coefficients are conjugate-symmetric under frequency negation, which is exactly what makes the kernel real-valued.

Integer-spectrum corollary

theorem QuantumAlg.overlapES_freq {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (σ : Fin (N + N) → ℝ) (hσ : σ ∈ (overlapES W lam ψ).freqs) : (∀ (a : Fin N), ∃ (μ : Fin d), σ (Fin.castAdd N a) = -lam μ) ∧ ∀ (a : Fin N), ∃ (ν : Fin d), σ (Fin.natAdd N a) = lam ν

Every overlap frequency is a negated eigenvalue on the first block and an eigenvalue on the second block.

theorem QuantumAlg.fourier_integer_spectrum {N d : ℕ} (W : Fin (N + 1) → Matrix (Fin d) (Fin d) ℂ) (lam : Fin d → ℝ) (ψ : Fin d → ℂ) (hint : ∀ (i j : Fin d), ∃ (z : ℤ), lam i - lam j = ↑z) (σ : Fin (N + N) → ℝ) (hσ : σ ∈ (kernelES W lam ψ).freqs) (a : Fin (N + N)) : ∃ (z : ℤ), σ a = ↑z

Integer-spectrum corollary (Schuld 2021). If every eigenvalue difference is an integer, every kernel frequency has integer coordinates — the kernel is a genuine multidimensional Fourier series.

Non-vacuity witness: the Pauli-X encoding reproduces the cos² kernel

noncomputable def QuantumAlg.pauliXSpectrum : Fin 2 → ℝ

Eigenvalues of ½σ_x: (-1/2, 1/2).

Equations

• QuantumAlg.pauliXSpectrum = ![-(1 / 2), 1 / 2]

noncomputable def QuantumAlg.pauliXPsi : Fin 2 → ℂ

Uniform initial state (1/√2, 1/√2).

Equations

• QuantumAlg.pauliXPsi = ![↑(√2)⁻¹, ↑(√2)⁻¹]

noncomputable def QuantumAlg.pauliXW : Fin 2 → Matrix (Fin 2) (Fin 2) ℂ

Trivial surrounding unitaries (identity): the data is encoded by the diagonal gate alone.

Equations

• QuantumAlg.pauliXW = ![1, 1]

theorem QuantumAlg.pauliX_featState (x : ℝ) : featState pauliXW pauliXSpectrum pauliXPsi 1 ![x] = ![↑(√2)⁻¹ * Complex.exp (Complex.I * ↑(x / 2)), ↑(√2)⁻¹ * Complex.exp (-(Complex.I * ↑(x / 2)))]

The single-qubit cosine-encoding feature state is (e^{ix/2}/√2, e^{-ix/2}/√2).

theorem QuantumAlg.pauliX_kernel_eq_cos_sq (x x' : ℝ) : Complex.normSq (∑ m : Fin 2, (starRingEnd ℂ) (featState pauliXW pauliXSpectrum pauliXPsi 1 ![x'] m) * featState pauliXW pauliXSpectrum pauliXPsi 1 ![x] m) = Real.cos ((x - x') / 2) ^ 2

Non-vacuity witness (Schuld 2021). The single-qubit cosine-encoding quantum kernel equals the squared-cosine kernel cos²((x-x')/2).