The vocabulary of the Hilbert space inequality

The objects of the source's key proposition, which speaks only of a finite conjugation-invariant multiset of complex numbers and a test function — no zeta function appears.

A multiset is presented by its finite support Z together with a multiplicity function m, so every sum is written over a finite set with explicit weights. That is what removes the source's bookkeeping over conjugate pairs: because gz is conjugation-invariant and hz anti-invariant, a sum over the whole non-real part equals twice a sum over representatives, with no choice of representatives to make.

noncomputable def ZetaZeros.fz (eta : ℝ → ℝ) (z : ℂ) (u : ℝ) : ℂ

The Fourier transform of a compactly supported real function, at a complex argument.

Equations

• ZetaZeros.fz eta z u = ↑(eta u) * Complex.exp (-(2 * ↑Real.pi) * Complex.I * ↑u * z)

noncomputable def ZetaZeros.gz (eta : ℝ → ℝ) (z : ℂ) (u : ℝ) : ℂ

The even part of the twisted pair, gz = (fz z + fz (conj z)) / 2.

Equations

• ZetaZeros.gz eta z u = (ZetaZeros.fz eta z u + ZetaZeros.fz eta ((starRingEnd ℂ) z) u) / 2

noncomputable def ZetaZeros.hz (eta : ℝ → ℝ) (z : ℂ) (u : ℝ) : ℂ

The odd part of the twisted pair, hz = (fz z - fz (conj z)) / (2i).

Equations

• ZetaZeros.hz eta z u = (ZetaZeros.fz eta z u - ZetaZeros.fz eta ((starRingEnd ℂ) z) u) / (2 * Complex.I)

def ZetaZeros.IsSymmetric (Φ : ℝ → ℂ) : Prop

A function ℝ → ℂ is symmetric when conjugation acts as reflection: conj (Φ u) = Φ (-u). The property is preserved by Gram–Schmidt and is what makes the Bessel coefficients real.

Equations

• ZetaZeros.IsSymmetric Φ = ∀ (u : ℝ), (starRingEnd ℂ) (Φ u) = Φ (-u)

noncomputable def ZetaZeros.bigF (eta : ℝ → ℝ) (Z : Finset ℂ) (m : ℂ → ℕ) (u v : ℝ) : ℂ

The two-variable kernel F (u, v) = ∑ z, m z * fz z u * fz z v, the multiset sum written with explicit multiplicities.

Equations

• ZetaZeros.bigF eta Z m u v = ∑ z ∈ Z, ↑(m z) * ZetaZeros.fz eta z u * ZetaZeros.fz eta z v

noncomputable def ZetaZeros.multipleRealPart (Z : Finset ℂ) (m : ℂ → ℕ) : Finset ℂ

The simple real part of the support: real points of multiplicity one.

Equations

• ZetaZeros.multipleRealPart Z m = {x ∈ Z | x.im = 0 ∧ 2 ≤ m x}

noncomputable def ZetaZeros.nonRealPart (Z : Finset ℂ) : Finset ℂ

The non-real part of the support.

Equations

• ZetaZeros.nonRealPart Z = {z ∈ Z | z.im ≠ 0}

theorem ZetaZeros.gz_conj (eta : ℝ → ℝ) (z : ℂ) : gz eta ((starRingEnd ℂ) z) = gz eta z

The even part is conjugation-invariant.

theorem ZetaZeros.hz_conj (eta : ℝ → ℝ) (z : ℂ) : hz eta ((starRingEnd ℂ) z) = fun (u : ℝ) => -hz eta z u

The odd part is conjugation-anti-invariant.

theorem ZetaZeros.fz_eq_gz_add_I_mul_hz (eta : ℝ → ℝ) (z : ℂ) (u : ℝ) : fz eta z u = gz eta z u + Complex.I * hz eta z u

The twisted function splits into its even and odd parts: fz = gz + i * hz.