A variant of the configuration inequality (6.9)

From the raw inequality energy_raw with ε = K⁻⁶, the potential inequality potential_ineq (Lemma 6.1), the tail bound (6.8) and the bound for the regularisation error we obtain energy_ineq_final: for every configuration of h = 37 n positive, pairwise distinct points,

2∑_{i<j} log|tᵢ - tⱼ| - K∑V(tᵢ) + ∑√tᵢ ≤ (λM₀ - I(ρ))K² + 5h + 6h log K.

The paper uses (120 + √2)h + 2h log K for the lower-order terms and ε = K⁻². Here the different regularisation estimate and ε = K⁻⁶ give 5h + 6h log K.

theorem Zeta5Irrational.sqrt_add_le' {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : √(a + b) ≤ √a + √b

theorem Zeta5Irrational.errj_le {ε t m r : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (ht : 0 < t) (hm : 0 < m ∧ m < 2) (hr : 1 / 450 ≤ r) : errj ε t m r ≤ √ε * (637 * √t + 1457)

The regularisation error at one interval.

theorem Zeta5Irrational.sum_cρ_fin : ∑ j : Fin 16, cρ (↑j + 1) = lam

The total mass of the sixteen weights.

theorem Zeta5Irrational.Err_le {ε t : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (ht : 0 < t) : Err ε t ≤ √ε * (590 * √t + 1348)

The total regularisation error.

theorem Zeta5Irrational.potential_ineq_tail' {t c : ℝ} (ht : 2 ≤ t) (_hc0 : 0 ≤ c) (hc : c ≤ 1 / 20) : 2 * Uρ t - Vfield t + c * √t ≤ M0

The tail bound with an extra c √t, 0 ≤ c ≤ 1/20.

theorem Zeta5Irrational.pointwise_bound {K t : ℝ} (hK : 40 ≤ K) (ht : 0 < t) : 2 * Uρ t - Vfield t + 2 / K * √t ≤ M0 + 3 / K

A variant of (6.7): 2Uρ(t) - V(t) + (2/K)√t ≤ M₀ + 3/K for K ≥ 40. The paper instead uses √t/K and √2/K, and assumes K ≥ 2.

theorem Zeta5Irrational.sum_pairs_eq {h : ℕ} (t : Fin h → ℝ) : ∑ i : Fin h, ∑ i' : Fin h, Real.log |t i - t i'| = ∑ i : Fin h, ∑ j > i, 2 * Real.log |t j - t i|

The double sum over all ordered pairs equals twice the sum over i < j.

theorem Zeta5Irrational.energy_ineq_final (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, for positive pairwise distinct configurations and K = 40n.