The four blocks of the configuration energy

With P k l = pairInt (atomγ t ε) (log ‖· - ·‖) k l:

• (A) P (inl i) (inl i) = (2π)² log ε;
• (B) (2π)² log |tᵢ - tᵢ'| ≤ P (inl i) (inl i') for tᵢ ≠ tᵢ';
• (C) P (inl i) (inr j) ≤ (2π)² (Uω aⱼ bⱼ tᵢ + errⱼ(tᵢ)) (circle regularisation error);
• (D) (2π)² log ((bⱼ' - aⱼ')/4) ≤ P (inr j) (inr j').

noncomputable def Zeta5Irrational.Plog {h : ℕ} (t : Fin h → ℝ) (ε : ℝ) (k l : Idx h) : ℝ

The pair integrals of the logarithmic kernel for the configuration atoms.

Equations

• Zeta5Irrational.Plog t ε k l = Zeta5Irrational.pairInt (Zeta5Irrational.atomγ t ε) (fun (z w : ℂ) => Real.log ‖z - w‖) k l

theorem Zeta5Irrational.log_le_log_add_posLog {ε x : ℝ} (hε : 0 < ε) (hx : 0 < x) : Real.log x ≤ Real.log ε + (ε⁻¹ * x).posLog

theorem Zeta5Irrational.inner_intervalIntegrable {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (k l : Idx h) : IntervalIntegrable (fun (θ : ℝ) => ∫ (φ : ℝ) in 0..2 * Real.pi, Real.log ‖atomγ t ε k θ - atomγ t ε l φ‖) MeasureTheory.volume 0 (2 * Real.pi)

The inner integrals are interval integrable in the outer variable.

theorem Zeta5Irrational.norm_circleMap_sub_center' (c : ℝ) {ε : ℝ} (hε : 0 < ε) (θ : ℝ) : ‖↑c - circleMap (↑c) ε θ‖ = ε

theorem Zeta5Irrational.circle_log_integral' (c a : ℂ) {R : ℝ} (hR : R ≠ 0) : ∫ (θ : ℝ) in 0..2 * Real.pi, Real.log ‖a - circleMap c R θ‖ = 2 * Real.pi * (Real.log R + (R⁻¹ * ‖c - a‖).posLog)

theorem Zeta5Irrational.block_A {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (i : Fin h) : Plog t ε (Sum.inl i) (Sum.inl i) = (2 * Real.pi) ^ 2 * Real.log ε

(A): the self-energy of a circle.

theorem Zeta5Irrational.block_B {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (i i' : Fin h) (hne : t i ≠ t i') : (2 * Real.pi) ^ 2 * Real.log |t i - t i'| ≤ Plog t ε (Sum.inl i) (Sum.inl i')

(B): the mutual energy of two circles dominates log |tᵢ - tᵢ'|.

noncomputable def Zeta5Irrational.errj (ε t m r : ℝ) : ℝ

The regularisation error of the arcsine potential at a real point t.

Equations

• Zeta5Irrational.errj ε t m r = ε / r + √(ε / r * ((ε + 2 * |t - m|) / r))

theorem Zeta5Irrational.errj_nonneg {ε t m r : ℝ} (hε : 0 < ε) (hr : 0 < r) : 0 ≤ errj ε t m r

theorem Zeta5Irrational.block_C {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (i : Fin h) (j : Fin 16) : Plog t ε (Sum.inl i) (Sum.inr j) ≤ (2 * Real.pi) ^ 2 * (Uω (aρ (↑j + 1)) (bρ (↑j + 1)) (t i) + errj ε (t i) (mρ (↑j + 1)) (rρ (↑j + 1)))

(C): circle–arcsine energy.

theorem Zeta5Irrational.log_le_Uω {a b : ℝ} (hab : a < b) (t : ℝ) : Real.log ((b - a) / 4) ≤ Uω a b t

Uω a b t ≥ log ((b - a)/4) for all t.

theorem Zeta5Irrational.block_D {h : ℕ} (t : Fin h → ℝ) {ε : ℝ} (hε : 0 < ε) (j j' : Fin 16) : (2 * Real.pi) ^ 2 * Real.log ((bρ (↑j' + 1) - aρ (↑j' + 1)) / 4) ≤ Plog t ε (Sum.inr j) (Sum.inr j')

(D): arcsine–arcsine energy is at least log ((bⱼ' - aⱼ')/4).