Reducing the functional to a single integral against G

Q_0 0 is the integral of f_0 squared and the moment term is the double integral of |u - v| f_0 u f_0 v; added, they are the integral of f_0 against G.

theorem ZetaZeros.extremalSelfConv_eq_interval (α : ℝ) : extremalSelfConv α = ∫ (t : ℝ) in -1 / 2..1 / 2, extremalTest t * extremalTest (α - t)

The self-convolution restricted to the support interval.

theorem ZetaZeros.step1_selfconv0 : extremalSelfConv 0 = ∫ (u : ℝ) in -1 / 2..1 / 2, extremalTest u * extremalTest u

Part (I): Q₀(0) = ∫_{-1/2}^{1/2} f₀(u)² du.

theorem ZetaZeros.inner_reduce {t : ℝ} (ht : |t| ≤ 1 / 2) : ∫ (α : ℝ) in 0..1, α * extremalTest (α - t) = ∫ (β : ℝ) in -1 / 2..1 / 2, max (β + t) 0 * extremalTest β

Inner reduction: substituting β = α - t and using the support of extremalTest, ∫ α in 0..1, α · f₀(α - t) = ∫ β in -1/2..1/2, max(β+t, 0) · f₀(β) for |t| ≤ 1/2.

theorem ZetaZeros.step1_double : 2 * ∫ (α : ℝ) in 0..1, α * extremalSelfConv α = ∫ (u : ℝ) in -1 / 2..1 / 2, extremalTest u * ∫ (v : ℝ) in -1 / 2..1 / 2, |u - v| * extremalTest v

Part (II): 2 ∫₀¹ α Q₀(α) dα = ∫∫ |u-v| f₀(u) f₀(v).

theorem ZetaZeros.montgomeryTaylor_step1 : extremalSelfConv 0 + 2 * ∫ (α : ℝ) in 0..1, α * extremalSelfConv α = ∫ (u : ℝ) in -1 / 2..1 / 2, extremalTest u * extremalG u