Variants of the energy bound (6.14) and configuration inequality (6.9)

• energy_ineq: a variant of (6.9), with 5h + 6h log K replacing (120 + √2)h + 2h log K, for positive pairwise distinct configurations. It follows from energy_ineq_final (Lemma 6.1, Lemma 6.2, circle regularisation).
• log_Δ_le': a variant of (6.14), with 22 h log K + 50 h replacing 18 h log K + 160 h.
• everything else: the pointwise bound for the integrand of (6.10) and its integration.

theorem Zeta5Irrational.energy_ineq (n : ℕ) (hn : 0 < n) (t : Fin (37 * n) → ℝ) (ht : ∀ (i : Fin (37 * n)), 0 < t i) (hinj : Function.Injective t) : ∑ i : Fin (37 * n), ∑ j > i, 2 * Real.log |t j - t i| - Kr n * ∑ i : Fin (37 * n), Vfield (t i) + ∑ i : Fin (37 * n), √(t i) ≤ (lam * M0 - Irho) * Kr n ^ 2 + 5 * (37 * ↑n) + 6 * (37 * ↑n) * Real.log (Kr n)

A variant of (6.9) with lower-order terms 5h + 6h log K instead of (120 + √2)h + 2h log K, as proved in energy_ineq_final.

theorem Zeta5Irrational.aeval_D_eq (m : ℕ) (s : ℝ) : (Polynomial.aeval s) (D m) = ∏ j ∈ Finset.Icc 1 m, (s + ↑j ^ 2)

theorem Zeta5Irrational.sum_Ioi_card_mul_two (h : ℕ) : (∑ i : Fin h, (Finset.Ioi i).card) * 2 = h * (h - 1)

theorem Zeta5Irrational.sum_Ioi_const (h : ℕ) (c : ℝ) : ∑ i : Fin h, ∑ _j > i, c = ↑h * (↑h - 1) / 2 * c

theorem Zeta5Irrational.log_aeval_D (m : ℕ) {K y : ℝ} (hK : 0 < K) (hy : 0 < y) : Real.log ((Polynomial.aeval (y ^ 2)) (D m)) = 2 * ↑m * Real.log K + ∑ j ∈ Finset.range m, Real.log ((y / K) ^ 2 + ((↑j + 1) / K) ^ 2)

log D_m(y²) = 2m log K + ∑_{j<m} log(t + ((j+1)/K)²) with t = (y/K)².

noncomputable def Zeta5Irrational.Aconst (n : ℕ) : ℝ

The constant A_n in the pointwise bound.

Equations

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

noncomputable def Zeta5Irrational.gK (n : ℕ) (y : ℝ) : ℝ

The one-dimensional factor (1 + 2πy)^5 e^{-y/K}.

Equations

• Zeta5Irrational.gK n y = (1 + 2 * Real.pi * y) ^ 5 * Real.exp (-(1 / Zeta5Irrational.Kr n * y))

theorem Zeta5Irrational.integrand_le (n : ℕ) (hn : 0 < n) (y : Fin (37 * n) → ℝ) (hy : ∀ (i : Fin (37 * n)), 0 < y i) (hinj : Function.Injective y) : (Matrix.vandermonde fun (j : Fin (37 * n)) => y j ^ 2).det ^ 2 * ∏ j : Fin (37 * n), ν n (y j) ≤ Real.exp (Aconst n) * ∏ i : Fin (37 * n), gK n (y i)

Pointwise bound for the integrand of (6.10), for positive pairwise distinct y.

theorem Zeta5Irrational.integrableOn_gK (n : ℕ) (hn : 0 < n) : MeasureTheory.IntegrableOn (gK n) (Set.Ioi 0) MeasureTheory.volume

theorem Zeta5Irrational.log_C_le : Real.log ((2 * Real.pi) ^ 5 * 32 * 121) ≤ 18

log ((2π)^5 · 32 · 121) ≤ 18.

theorem Zeta5Irrational.log_Δ_le' (n : ℕ) (hn : 0 < n) : Real.log ((Polynomial.aeval zeta5) (Δ n)) ≤ 2 * (37 * ↑n) * (37 * ↑n + 6 * (3 * ↑n) - 40 * ↑n) * Real.log (Kr n) + (lam * M0 - Irho) * Kr n ^ 2 + 22 * (37 * ↑n) * Real.log (Kr n) + 50 * (37 * ↑n)

A variant of (6.14) with 22 h log K + 50 h instead of 18 h log K + 160 h: the energy bound for Δ_K(ζ(5)) from energy_ineq.