Towards the energy bound (6.14): elementary ingredients

• the external field V(t) = 2π√t + ∫₀¹ log(t+u²) du - 6 ∫₀^α log(t+u²) du of (6.1);
• the bound w(y) ≤ (1/π) (1 + 2πy)^5 e^{-2πy} (a form of (6.11));
• a variant of the sum–integral comparison (6.12) for u ↦ log (t + u²), using 2 log(2K) + 2 in place of 2 log K + 2 in the upper error bound.

noncomputable def Zeta5Irrational.Vfield (t : ℝ) : ℝ

The external field of (6.1).

Equations

• Zeta5Irrational.Vfield t = (2 * Real.pi * √t + ∫ (u : ℝ) in 0..1, Real.log (t + u ^ 2)) - 6 * ∫ (u : ℝ) in 0..3 / 40, Real.log (t + u ^ 2)

theorem Zeta5Irrational.w_le' {y : ℝ} (hy : 0 < y) : w y ≤ 1 / Real.pi * (1 + 2 * Real.pi * y) ^ 5 * Real.exp (-(2 * Real.pi * y))

w(y) ≤ (1/π) (1 + 2πy)^5 e^{-2πy} for y > 0.

theorem Zeta5Irrational.integral_le_sum_log {t : ℝ} (ht : 0 < t) {K : ℝ} (hK : 0 < K) (m : ℕ) : K * ∫ (u : ℝ) in 0..↑m / K, Real.log (t + u ^ 2) ≤ ∑ j ∈ Finset.range m, Real.log (t + ((↑j + 1) / K) ^ 2)

The monotone comparison (6.12): for t > 0 and 1 ≤ m, K ∫₀^{m/K} log(t+u²) du ≤ ∑_{j=1}^m log(t + (j/K)²).

theorem Zeta5Irrational.sum_log_le_integral {t : ℝ} (ht : 0 < t) {K : ℝ} (hK : 1 ≤ K) {m : ℕ} (hm : 1 ≤ m) (hmK : ↑m ≤ K) : ∑ j ∈ Finset.range m, Real.log (t + ((↑j + 1) / K) ^ 2) ≤ (K * ∫ (u : ℝ) in 0..↑m / K, Real.log (t + u ^ 2)) + 2 * Real.log (2 * K) + 2

A weakening of the reverse comparison (6.12): for t > 0, 1 ≤ m ≤ K, ∑_{j=1}^m log(t + (j/K)²) ≤ K ∫₀^{m/K} log(t+u²) du + 2 log(2K) + 2. The paper has the sharper remainder 2 log K + 2.

theorem Zeta5Irrational.integral_one_add_pow_mul_exp {K : ℝ} (hK : 1 ≤ K) : ∫ (y : ℝ) in Set.Ioi 0, (1 + 2 * Real.pi * y) ^ 5 * Real.exp (-(1 / K * y)) ≤ (2 * Real.pi) ^ 5 * 32 * 121 * K ^ 6

∫₀^∞ (1 + 2πy)^5 e^{-y/K} dy ≤ (2π)^5 · 32 · 121 · K^6 for K ≥ 1.

Almost every configuration has positive, pairwise distinct coordinates

theorem Zeta5Irrational.volume_eq_coord_null {h : ℕ} {i j : Fin h} (hij : i ≠ j) : MeasureTheory.volume {x : Fin h → ℝ | x i = x j} = 0

The hyperplane {x | x i = x j} is null for Lebesgue measure on Fin h → ℝ.

theorem Zeta5Irrational.ae_pos_injective (h : ℕ) : ∀ᵐ (x : Fin h → ℝ) ∂MeasureTheory.Measure.pi fun (x : Fin h) => μpos, (∀ (i : Fin h), 0 < x i) ∧ Function.Injective x

Almost every x (for dy on (0,∞)^h) has positive, pairwise distinct coordinates.