The kernel as an inner product

The identity that turns the kernel into a Gram matrix on L²((-lam, lam)), and its two immediate consequences.

Every integral here is taken over Set.Ioo (-lam) lam rather than over ℝ, so that it is literally the inner product of the ambient Hilbert space; fourierC integrates over the line, and the two agree because an admissible test function vanishes off the interval.

theorem ZetaZeros.testKernel_sub_conj {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z s : ℂ) : testKernel eta (z - (starRingEnd ℂ) s) = ∫ (u : ℝ) in Set.Ioo (-lam) lam, fz eta z u * (starRingEnd ℂ) (fz eta s u)

The kernel is a Gram matrix. K_eta (z - conj s) is the inner product of the twisted functions attached to z and s.

theorem ZetaZeros.integral_norm_fz_sq {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) {x : ℂ} (hx : x.im = 0) : ∫ (u : ℝ) in Set.Ioo (-lam) lam, ‖fz eta x u‖ ^ 2 = 1

At a real point the twisted function has unit L² norm.

theorem ZetaZeros.sum_testKernel_sq_eq_sum_conj {eta : ℝ → ℝ} {Z : Finset ℂ} {m : ℂ → ℕ} (h : IsConjInvariant Z m) : ∑ z ∈ Z, ∑ s ∈ Z, ↑(m z) * ↑(m s) * testKernel eta (z - s) ^ 2 = ∑ z ∈ Z, ∑ s ∈ Z, ↑(m z) * ↑(m s) * testKernel eta (z - (starRingEnd ℂ) s) ^ 2

Conjugating the second argument of the kernel does not change the second moment: conjugation permutes the support and preserves multiplicity.