The zeta-side vocabulary

The zero counts, the pair-correlation apparatus, and the kernel construction of the source's Section 3.

Every definition that also appears in Challenge/Basic.lean is spelled identically here. That is a requirement rather than a courtesy: the comparator compares elaborated types, so a development and a challenge that spell one notion two ways name two constants, and the pair then verifies nothing while every other gate stays green.

noncomputable def ZetaZeros.rescale (T : ℝ) (ρ : ℂ) : ℂ

The non-trivial zeros of the Riemann zeta function with imaginary part in (0, T]: the zeros lying in the critical strip 0 < re s < 1, as a set, so without multiplicity.

Equations

• ZetaZeros.rescale T ρ = Complex.I * (ρ - 1 / 2) * ↑(Real.log T / (2 * Real.pi))

noncomputable def ZetaZeros.rescaledZeros (T : ℝ) : Set ℂ

The rescaled zeros: the image of the non-trivial zeros up to height T.

Equations

• ZetaZeros.rescaledZeros T = ZetaZeros.rescale T '' ZetaZeros.nontrivialZeros T

noncomputable def ZetaZeros.rescaledMult (T : ℝ) (w : ℂ) : ℕ

The multiplicity transported along the rescaling: the rescaling is injective, so a rescaled point inherits the multiplicity of the zero it came from.

Equations

• ZetaZeros.rescaledMult T w = ZetaZeros.zeroMultiplicity (w / (Complex.I * ↑(Real.log T / (2 * Real.pi))) + 1 / 2)

noncomputable def ZetaZeros.extremalTest (x : ℝ) : ℝ

The extremal test function cos(√2 x) / (√2 sin(1/√2)) on [-1/2, 1/2], zero elsewhere.

Equations

• ZetaZeros.extremalTest x = if |x| ≤ 1 / 2 then Real.cos (√2 * x) / (√2 * Real.sin (1 / √2)) else 0

noncomputable def ZetaZeros.extremalSelfConv (x : ℝ) : ℝ

The self-convolution of the extremal test function.

Equations

• ZetaZeros.extremalSelfConv x = ∫ (t : ℝ), ZetaZeros.extremalTest t * ZetaZeros.extremalTest (x - t)

structure ZetaZeros.IsCutoff (delta : ℝ) (psi : ℝ → ℝ) : Prop

psi is a delta-cutoff: smooth, even, supported in (-1/2, 1/2), valued in [0, 1], and identically 1 on |x| ≤ 1/2 - delta.

• smooth : ContDiff ℝ (↑⊤) psi

  psi is smooth.

• support (x : ℝ) : 1 / 2 ≤ |x| → psi x = 0

  psi vanishes off (-1/2, 1/2).

• even (x : ℝ) : psi (-x) = psi x

  psi is even.

• nonneg (x : ℝ) : 0 ≤ psi x

  psi is non-negative.

• le_one (x : ℝ) : psi x ≤ 1

  psi is at most one.

• eq_one (x : ℝ) : |x| ≤ 1 / 2 - delta → psi x = 1

  psi is identically one on the shrunken interval.

noncomputable def ZetaZeros.cutoffNormaliser (psi : ℝ → ℝ) : ℝ

The normalising constant A_psi = ∫ psi² f₀.

Equations

• ZetaZeros.cutoffNormaliser psi = ∫ (x : ℝ), psi x ^ 2 * ZetaZeros.extremalTest x

noncomputable def ZetaZeros.cutoffTest (psi : ℝ → ℝ) (x : ℝ) : ℝ

The normalised test function eta_psi = psi √f₀ / √A_psi.

Equations

• ZetaZeros.cutoffTest psi x = psi x * √(ZetaZeros.extremalTest x) / √(ZetaZeros.cutoffNormaliser psi)

noncomputable def ZetaZeros.cutoffTestSq (psi : ℝ → ℝ) : ℝ → ℝ

Its square, f_psi = eta_psi².

Equations

• ZetaZeros.cutoffTestSq psi = ZetaZeros.cutoffTest psi ^ 2

noncomputable def ZetaZeros.cutoffSelfConv (psi : ℝ → ℝ) (x : ℝ) : ℝ

Its self-convolution, Q_psi = f_psi ⋆ f_psi.

Equations

• ZetaZeros.cutoffSelfConv psi x = ∫ (t : ℝ), ZetaZeros.cutoffTestSq psi t * ZetaZeros.cutoffTestSq psi (x - t)

noncomputable def ZetaZeros.correctedTest (psi : ℝ → ℝ) (T x : ℝ) : ℝ

The corrected test function r_{psi,T} = Q_psi - Q_psi'' / (4 (log T)²), whose Fourier transform carries the factor that cancels the pair-correlation weight.

Equations

• ZetaZeros.correctedTest psi T x = ZetaZeros.cutoffSelfConv psi x - iteratedDeriv 2 (ZetaZeros.cutoffSelfConv psi) x / (4 * Real.log T ^ 2)