Trigonometric polynomials

A trigonometric polynomial in k real variables is a finite ℂ-linear combination of the characters x ↦ exp (i ⟨ω, x⟩), where the frequency vectors ω range over a finite set. These are exactly the trigonometric polynomials, and they are closed under addition, scaling, multiplication by a single character, products, and complex conjugation — the algebraic facts that drive the Fourier representation of the quantum kernel.

This module is quantum-free: it only knows about ℂ, finite sums, the real pairing ⟨ω, x⟩ = ∑ i, ω i * x i, and real one-variable trigonometric identities.

def QuantumAlg.freqDot {k : ℕ} (ω x : Fin k → ℝ) : ℝ

The real pairing ⟨ω, x⟩ = ∑ i, ω i * x i of a frequency vector with a data point.

Equations

• QuantumAlg.freqDot ω x = ∑ i : Fin k, ω i * x i

structure QuantumAlg.TrigPolynomial (k : ℕ) : Type

An trigonometric polynomial in k real variables: the function x ↦ ∑_{ω ∈ freqs} coeff ω · exp(i⟨ω, x⟩). The data is a finite set of frequency vectors together with a complex coefficient at each.

• freqs : Finset (Fin k → ℝ)

  The finite set of frequency vectors carrying nonzero (or bookkept) coefficients.

• coeff : (Fin k → ℝ) → ℂ

  The complex coefficient at each frequency.

noncomputable def QuantumAlg.TrigPolynomial.eval {k : ℕ} (f : TrigPolynomial k) (x : Fin k → ℝ) : ℂ

Evaluate an trigonometric polynomial at a data point x.

Equations

• f.eval x = ∑ ω ∈ f.freqs, f.coeff ω * Complex.exp (Complex.I * ↑(QuantumAlg.freqDot ω x))

theorem QuantumAlg.freqDot_add {k : ℕ} (ω₁ ω₂ x : Fin k → ℝ) : freqDot (ω₁ + ω₂) x = freqDot ω₁ x + freqDot ω₂ x

The pairing is additive in the frequency argument.

theorem QuantumAlg.freqDot_neg {k : ℕ} (ω x : Fin k → ℝ) : freqDot (-ω) x = -freqDot ω x

The pairing negates with the frequency argument.

theorem QuantumAlg.freqDot_add_right {k : ℕ} (ω x₁ x₂ : Fin k → ℝ) : freqDot ω (x₁ + x₂) = freqDot ω x₁ + freqDot ω x₂

The pairing is additive in the data argument.

theorem QuantumAlg.freqDot_comm {k : ℕ} (ω x : Fin k → ℝ) : freqDot ω x = freqDot x ω

The pairing is symmetric.

def QuantumAlg.TrigPolynomial.zero {k : ℕ} : TrigPolynomial k

The zero trigonometric polynomial (empty frequency set).

Equations

• QuantumAlg.TrigPolynomial.zero = { freqs := ∅, coeff := fun (x : Fin k → ℝ) => 0 }

@[simp]

theorem QuantumAlg.TrigPolynomial.eval_zero {k : ℕ} (x : Fin k → ℝ) : zero.eval x = 0

def QuantumAlg.TrigPolynomial.smul {k : ℕ} (c : ℂ) (f : TrigPolynomial k) : TrigPolynomial k

Scale an trigonometric polynomial by a complex constant.

Equations

• QuantumAlg.TrigPolynomial.smul c f = { freqs := f.freqs, coeff := fun (ω : Fin k → ℝ) => c * f.coeff ω }

theorem QuantumAlg.TrigPolynomial.eval_smul {k : ℕ} (c : ℂ) (f : TrigPolynomial k) (x : Fin k → ℝ) : (smul c f).eval x = c * f.eval x

noncomputable def QuantumAlg.TrigPolynomial.add {k : ℕ} (f g : TrigPolynomial k) : TrigPolynomial k

Sum of two trigonometric polynomials: union of frequencies, with guarded coefficients added.

Equations

• f.add g = { freqs := f.freqs ∪ g.freqs, coeff := fun (ω : Fin k → ℝ) => (if ω ∈ f.freqs then f.coeff ω else 0) + if ω ∈ g.freqs then g.coeff ω else 0 }

theorem QuantumAlg.TrigPolynomial.eval_add {k : ℕ} (f g : TrigPolynomial k) (x : Fin k → ℝ) : (f.add g).eval x = f.eval x + g.eval x

noncomputable def QuantumAlg.TrigPolynomial.expMul {k : ℕ} (a : Fin k → ℝ) (f : TrigPolynomial k) : TrigPolynomial k

Multiply an trigonometric polynomial by the character e^{i⟨a,x⟩}: shifts every frequency by a and leaves the coefficients (re-indexed) unchanged.

Equations

• QuantumAlg.TrigPolynomial.expMul a f = { freqs := Finset.image (fun (ω : Fin k → ℝ) => ω + a) f.freqs, coeff := fun (ω : Fin k → ℝ) => f.coeff (ω - a) }

theorem QuantumAlg.TrigPolynomial.eval_expMul {k : ℕ} (a : Fin k → ℝ) (f : TrigPolynomial k) (x : Fin k → ℝ) : (expMul a f).eval x = Complex.exp (Complex.I * ↑(freqDot a x)) * f.eval x

noncomputable def QuantumAlg.TrigPolynomial.sum {k : ℕ} {ι : Type u_1} (s : Finset ι) (F : ι → TrigPolynomial k) : TrigPolynomial k

A finite sum of trigonometric polynomials: frequencies union over the index, with coefficients added.

Equations

• QuantumAlg.TrigPolynomial.sum s F = { freqs := s.biUnion fun (i : ι) => (F i).freqs, coeff := fun (ω : Fin k → ℝ) => ∑ i ∈ s, if ω ∈ (F i).freqs then (F i).coeff ω else 0 }

theorem QuantumAlg.TrigPolynomial.eval_sum {k : ℕ} {ι : Type u_1} (s : Finset ι) (F : ι → TrigPolynomial k) (x : Fin k → ℝ) : (sum s F).eval x = ∑ i ∈ s, (F i).eval x

noncomputable def QuantumAlg.TrigPolynomial.mul {k : ℕ} (f g : TrigPolynomial k) : TrigPolynomial k

Product of two trigonometric polynomials: realised as the sum, over f's frequencies, of g shifted by that frequency and scaled by f's coefficient.

Equations

• f.mul g = QuantumAlg.TrigPolynomial.sum f.freqs fun (ω : Fin k → ℝ) => QuantumAlg.TrigPolynomial.smul (f.coeff ω) (QuantumAlg.TrigPolynomial.expMul ω g)

theorem QuantumAlg.TrigPolynomial.eval_mul {k : ℕ} (f g : TrigPolynomial k) (x : Fin k → ℝ) : (f.mul g).eval x = f.eval x * g.eval x

noncomputable def QuantumAlg.TrigPolynomial.conj {k : ℕ} (f : TrigPolynomial k) : TrigPolynomial k

Complex conjugate of an trigonometric polynomial: negate frequencies, conjugate coefficients.

Equations

• f.conj = { freqs := Finset.image (fun (ω : Fin k → ℝ) => -ω) f.freqs, coeff := fun (ω : Fin k → ℝ) => (starRingEnd ℂ) (f.coeff (-ω)) }

theorem QuantumAlg.TrigPolynomial.eval_conj {k : ℕ} (f : TrigPolynomial k) (x : Fin k → ℝ) : f.conj.eval x = (starRingEnd ℂ) (f.eval x)

noncomputable def QuantumAlg.TrigPolynomial.coeffAt {k : ℕ} (f : TrigPolynomial k) (ω : Fin k → ℝ) : ℂ

The canonical coefficient of an trigonometric polynomial at a frequency: its (guarded) contribution. Two trigonometric polynomials with the same values have the same canonical coefficients (coeffAt_eq_of_eval_eq).

Equations

• f.coeffAt ω = if ω ∈ f.freqs then f.coeff ω else 0

theorem QuantumAlg.freqDot_smul_single {k : ℕ} (ω : Fin k → ℝ) (t : ℝ) (j : Fin k) : freqDot ω (t • Pi.single j 1) = t * ω j

Pairing against a single scaled basis frequency picks out one coordinate.

theorem QuantumAlg.exp_I_real_inj {a b : ℝ} (h : ∀ (t : ℝ), Complex.exp (Complex.I * ↑(t * a)) = Complex.exp (Complex.I * ↑(t * b))) : a = b

If t ↦ exp(i t a) and t ↦ exp(i t b) agree for all real t, then a = b.

noncomputable def QuantumAlg.chiHom {k : ℕ} (ω : Fin k → ℝ) : Multiplicative (Fin k → ℝ) →* ℂ

The character x ↦ exp(i⟨ω,x⟩) as a monoid homomorphism from the additive group of data points (written multiplicatively) to ℂ.

Equations

• QuantumAlg.chiHom ω = { toFun := fun (y : Multiplicative (Fin k → ℝ)) => Complex.exp (Complex.I * ↑(QuantumAlg.freqDot ω (Multiplicative.toAdd y))), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem QuantumAlg.chiHom_apply {k : ℕ} (ω : Fin k → ℝ) (y : Multiplicative (Fin k → ℝ)) : (chiHom ω) y = Complex.exp (Complex.I * ↑(freqDot ω (Multiplicative.toAdd y)))

theorem QuantumAlg.chiHom_injective {k : ℕ} : Function.Injective chiHom

Distinct frequencies give distinct characters.

theorem QuantumAlg.expSum_coeff_zero_of_eval_zero {k : ℕ} {s : Finset (Fin k → ℝ)} {c : (Fin k → ℝ) → ℂ} (h : ∀ (x : Fin k → ℝ), ∑ ω ∈ s, c ω * Complex.exp (Complex.I * ↑(freqDot ω x)) = 0) (ω : Fin k → ℝ) : ω ∈ s → c ω = 0

Uniqueness of trigonometric-polynomial coefficients. A vanishing finite combination of the distinct characters has all coefficients zero (Dedekind's independence of characters).

theorem QuantumAlg.TrigPolynomial.coeffAt_eq_of_eval_eq {k : ℕ} {f g : TrigPolynomial k} (h : ∀ (x : Fin k → ℝ), f.eval x = g.eval x) (ω : Fin k → ℝ) : f.coeffAt ω = g.coeffAt ω

Two trigonometric polynomials with the same values have the same canonical coefficients.

theorem QuantumAlg.TrigPolynomial.coeffAt_conj {k : ℕ} (f : TrigPolynomial k) (ω : Fin k → ℝ) : f.conj.coeffAt ω = (starRingEnd ℂ) (f.coeffAt (-ω))

The canonical coefficient of a conjugated trigonometric polynomial negates the frequency and conjugates.

Frequency-set characterizations (for tracking which frequencies appear)

@[simp]

theorem QuantumAlg.TrigPolynomial.smul_freqs {k : ℕ} (c : ℂ) (f : TrigPolynomial k) : (smul c f).freqs = f.freqs

@[simp]

theorem QuantumAlg.TrigPolynomial.expMul_freqs {k : ℕ} (a : Fin k → ℝ) (f : TrigPolynomial k) : (expMul a f).freqs = Finset.image (fun (ω : Fin k → ℝ) => ω + a) f.freqs

@[simp]

theorem QuantumAlg.TrigPolynomial.conj_freqs {k : ℕ} (f : TrigPolynomial k) : f.conj.freqs = Finset.image (fun (ω : Fin k → ℝ) => -ω) f.freqs

@[simp]

theorem QuantumAlg.TrigPolynomial.sum_freqs {k : ℕ} {ι : Type u_1} (s : Finset ι) (F : ι → TrigPolynomial k) : (sum s F).freqs = s.biUnion fun (i : ι) => (F i).freqs

theorem QuantumAlg.TrigPolynomial.mul_freqs {k : ℕ} (f g : TrigPolynomial k) : (f.mul g).freqs = f.freqs.biUnion fun (ω : Fin k → ℝ) => Finset.image (fun (ν : Fin k → ℝ) => ν + ω) g.freqs

Embedding into more variables (for products of sums in disjoint variable blocks)

theorem QuantumAlg.freqDot_append_left {m n : ℕ} (ω x : Fin m → ℝ) (y : Fin n → ℝ) : freqDot (Fin.append ω 0) (Fin.append x y) = freqDot ω x

The pairing of left-block-supported frequencies sees only the first block.

theorem QuantumAlg.freqDot_append_right {m n : ℕ} (ω : Fin n → ℝ) (x : Fin m → ℝ) (y : Fin n → ℝ) : freqDot (Fin.append 0 ω) (Fin.append x y) = freqDot ω y

The pairing of right-block-supported frequencies sees only the second block.

noncomputable def QuantumAlg.TrigPolynomial.embedL {m n : ℕ} (f : TrigPolynomial m) : TrigPolynomial (m + n)

Embed an m-variable trigonometric polynomial into m + n variables on the first block.

Equations

• f.embedL = { freqs := Finset.image (fun (ω : Fin m → ℝ) => Fin.append ω 0) f.freqs, coeff := fun (σ : Fin (m + n) → ℝ) => f.coeff fun (i : Fin m) => σ (Fin.castAdd n i) }

noncomputable def QuantumAlg.TrigPolynomial.embedR {m n : ℕ} (f : TrigPolynomial n) : TrigPolynomial (m + n)

Embed an n-variable trigonometric polynomial into m + n variables on the second block.

Equations

• f.embedR = { freqs := Finset.image (fun (ω : Fin n → ℝ) => Fin.append 0 ω) f.freqs, coeff := fun (σ : Fin (m + n) → ℝ) => f.coeff fun (i : Fin n) => σ (Fin.natAdd m i) }

theorem QuantumAlg.TrigPolynomial.eval_embedL {m n : ℕ} (f : TrigPolynomial m) (x : Fin m → ℝ) (y : Fin n → ℝ) : f.embedL.eval (Fin.append x y) = f.eval x

theorem QuantumAlg.TrigPolynomial.eval_embedR {m n : ℕ} (f : TrigPolynomial n) (x : Fin m → ℝ) (y : Fin n → ℝ) : f.embedR.eval (Fin.append x y) = f.eval y

@[simp]

theorem QuantumAlg.TrigPolynomial.embedL_freqs {m n : ℕ} (f : TrigPolynomial m) : f.embedL.freqs = Finset.image (fun (ω : Fin m → ℝ) => Fin.append ω 0) f.freqs

@[simp]

theorem QuantumAlg.TrigPolynomial.embedR_freqs {m n : ℕ} (f : TrigPolynomial n) : f.embedR.freqs = Finset.image (fun (ω : Fin n → ℝ) => Fin.append 0 ω) f.freqs

One-variable parameter-shift identity

theorem QuantumAlg.trig_parameter_shift (a b c θ : ℝ) : deriv (fun (t : ℝ) => a + b * Real.cos t + c * Real.sin t) θ = (a + b * Real.cos (θ + Real.pi / 2) + c * Real.sin (θ + Real.pi / 2) - (a + b * Real.cos (θ - Real.pi / 2) + c * Real.sin (θ - Real.pi / 2))) / 2

Parameter-shift identity. The derivative of a + b cos θ + c sin θ equals the symmetric π/2-shifted finite difference (C(θ+π/2) - C(θ-π/2))/2.