Shared definitions used across the development. Arithmetic: colVal, allocCost, GreedyBound (the proof notes, Lemma 4 in allocation form). Analytic: Rfun, wfun, heineIntegrand, HeineBound (the proof notes, 5.2 in bound form).

def Zeta32.colVal (n p b : ℕ) : ℤ

Column value c_b = 4 N_b − C_b + [b = 0] − 2 of the proof notes, §3, with N_b = #{1 ≤ i ≤ n : i ≡ b} and C_b = #{1 ≤ j ≤ 5n : j ≡ b} modulo p.

Equations

• Zeta32.colVal n p b = (4 * ↑{i ∈ Finset.Icc 1 n | i % p = b}.card - ↑{j ∈ Finset.Icc 1 (5 * n) | j % p = b}.card + if b = 0 then 1 else 0) - 2

def Zeta32.allocCost (n p : ℕ) (k : ℕ → ℕ) : ℤ

Cost of taking the first k b entries c_b, c_b + 2, … of every column b < p.

Equations

• Zeta32.allocCost n p k = ∑ b ∈ Finset.range p, (↑(k b) * Zeta32.colVal n p b + ↑(k b) * (↑(k b) - 1))

def Zeta32.GreedyBound (r : ℚ) (n p : ℕ) : Prop

the proof notes, Lemma 4 in allocation form: some allocation of the h = 3n picks bounds every nonzero coefficient of Q r n from below p-adically (the greedy allocation does).

Equations

• Zeta32.GreedyBound r n p = ∃ (k : ℕ → ℕ), ∑ b ∈ Finset.range p, k b = 3 * n ∧ ∀ (i : ℕ), (Zeta32.Q r n).coeff i ≠ 0 → ↑(Zeta32.allocCost n p k) ≤ ↑(padicValRat p ((Zeta32.Q r n).coeff i))

noncomputable def Zeta32.Rfun (n : ℕ) (t : ℂ) : ℂ

R_n(t) = D_n(t)^4 / D_{5n}(t) as a complex function.

Equations

• Zeta32.Rfun n t = (∏ j ∈ Finset.Icc 1 n, (t + ↑j)) ^ 4 / ∏ j ∈ Finset.Icc 1 (5 * n), (t + ↑j)

noncomputable def Zeta32.wfun (r : ℚ) (y : ℝ) : ℂ

The kernel w(y) = (π/2) sech²(πy) (2r − 2πi tanh πy) of the proof notes, 5.1.

Equations

• Zeta32.wfun r y = ↑(Real.pi / 2 / Real.cosh (Real.pi * y) ^ 2) * (2 * ↑r - 2 * ↑Real.pi * Complex.I * ↑(Real.tanh (Real.pi * y)))

noncomputable def Zeta32.heineIntegrand (r : ℚ) (n : ℕ) (y : Fin (3 * n) → ℝ) : ℝ

∏_l |(t R_n)(t_l) w(y_l)| · Δ(y)² with t_l = 1/2 + i y_l, h = 3n.

Equations

• One or more equations did not get rendered due to their size.

def Zeta32.HeineBound (r : ℚ) (n : ℕ) : Prop

the proof notes, 5.2 (Heine), in the bound form used by 5.3.

Equations

• Zeta32.HeineBound r n = (|(Polynomial.aeval (Zeta32.Cr r)) (Zeta32.Q r n)| ≤ 1 / ↑(3 * n).factorial * ∫ (y : Fin (3 * n) → ℝ), Zeta32.heineIntegrand r n y)