The auxiliary kernel G, and why it is constant

G u = f_0 u + integral over [-1/2, 1/2] of |u - v| f_0 v.

The heart of the computation: the modulus kernel differentiates twice to 2 f_0 u while f_0'' = -2 f_0, so G'' = 0 and G is affine; being even, it is constant.

noncomputable def ZetaZeros.extremalG (u : ℝ) : ℝ

The auxiliary kernel G(u) = f₀(u) + ∫_{-1/2}^{1/2} |u - v| f₀(v) dv, which is constant on [-1/2, 1/2].

Equations

• ZetaZeros.extremalG u = ZetaZeros.extremalTest u + ∫ (v : ℝ) in -1 / 2..1 / 2, |u - v| * ZetaZeros.extremalTest v

Antiderivatives for the modulus kernel

theorem ZetaZeros.hasDerivAt_vcos (v : ℝ) : HasDerivAt (fun (v : ℝ) => v * Real.sin (√2 * v) / √2 + Real.cos (√2 * v) / 2) (v * Real.cos (√2 * v)) v

Antiderivative fact: d/dv [v sin(√2 v)/√2 + cos(√2 v)/2] = v cos(√2 v).

theorem ZetaZeros.hasDerivAt_shift (u v : ℝ) : HasDerivAt (fun (v : ℝ) => u * Real.sin (√2 * v) / √2 - (v * Real.sin (√2 * v) / √2 + Real.cos (√2 * v) / 2)) ((u - v) * Real.cos (√2 * v)) v

Antiderivative for the shifted kernel: for fixed u, d/dv [u·sin(√2 v)/√2 − (v·sin(√2 v)/√2 + cos(√2 v)/2)] = (u − v)·cos(√2 v).

theorem ZetaZeros.extremalG_const {u : ℝ} (hu : |u| ≤ 1 / 2) : extremalG u = extremalG 0