The raw configuration inequality

Combining atom_energy_nonpos with the four block estimates gives, for every configuration t : Fin (37 n) → ℝ of pairwise distinct points and every ε > 0:

∑ᵢ ∑ᵢ' log |tᵢ - tᵢ'| ≤ -h log ε + 2K ∑ᵢ (Uρ(tᵢ) + Err ε (tᵢ)) - K² I(ρ)

(energy_raw), where the diagonal terms are log 0 = 0.

noncomputable def Zeta5Irrational.Err (ε t : ℝ) : ℝ

The total regularisation error at a point.

Equations

• Zeta5Irrational.Err ε t = ∑ j : Fin 16, Zeta5Irrational.cρ (↑j + 1) * Zeta5Irrational.errj ε t (Zeta5Irrational.mρ (↑j + 1)) (Zeta5Irrational.rρ (↑j + 1))

theorem Zeta5Irrational.sum_sum_max_eq (c f : ℕ → ℝ) (N : ℕ) : ∑ j ∈ Finset.range N, ∑ j' ∈ Finset.range N, c j * c j' * f (max j j') = ∑ j ∈ Finset.range N, ((∑ i ∈ Finset.range (j + 1), c i) ^ 2 - (∑ i ∈ Finset.range j, c i) ^ 2) * f j

∑_{j,j' < N} c_j c_j' f (max j j') = ∑_{j < N} (S_{j+1}² - S_j²) f_j with S_k = ∑_{i<k} c_i.

theorem Zeta5Irrational.Irho_eq_double_sum : Irho = ∑ j : Fin 16, ∑ j' : Fin 16, cρ (↑j + 1) * cρ (↑j' + 1) * Real.log ((bρ (max ↑j ↑j' + 1) - aρ (max ↑j ↑j' + 1)) / 4)

I(ρ) as a double sum over the sixteen intervals.

theorem Zeta5Irrational.block_D_sum {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) : (2 * Real.pi) ^ 2 * Irho ≤ ∑ j : Fin 16, ∑ j' : Fin 16, cρ (↑j + 1) * cρ (↑j' + 1) * Plog t ε (Sum.inr j) (Sum.inr j')

The arcsine–arcsine block dominates (2π)² I(ρ).

theorem Zeta5Irrational.block_AB_sum {h : ℕ} (t : Fin h → ℝ) (hinj : Function.Injective t) {ε : ℝ} (hε : 0 < ε) : (2 * Real.pi) ^ 2 * (↑h * Real.log ε + ∑ i : Fin h, ∑ i' : Fin h, Real.log |t i - t i'|) ≤ ∑ i : Fin h, ∑ i' : Fin h, Plog t ε (Sum.inl i) (Sum.inl i')

The circle–circle block.

theorem Zeta5Irrational.block_C_sum {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (i : Fin h) : ∑ j : Fin 16, cρ (↑j + 1) * Plog t ε (Sum.inl i) (Sum.inr j) ≤ (2 * Real.pi) ^ 2 * (Uρ (t i) + Err ε (t i))

The circle–arcsine block.

theorem Zeta5Irrational.energy_raw (n : ℕ) (hn : 0 < n) (t : Fin (37 * n) → ℝ) (hinj : Function.Injective t) {ε : ℝ} (hε : 0 < ε) : ∑ i : Fin (37 * n), ∑ i' : Fin (37 * n), Real.log |t i - t i'| ≤ -(37 * ↑n) * Real.log ε + 2 * Kr n * ∑ i : Fin (37 * n), (Uρ (t i) + Err ε (t i)) - Kr n ^ 2 * Irho

The raw configuration inequality.