The tail t ≥ 2 of the potential inequality (6.2): the bound (6.8)

theorem Zeta5Irrational.Uω_le_log {a b t : ℝ} (ha : 0 < a) (hab : a < b) (h : b ≤ t) : Uω a b t ≤ Real.log t

For t ≥ b, Uω a b t ≤ log t.

theorem Zeta5Irrational.Uρ_le_log {t : ℝ} (ht : 2 ≤ t) : Uρ t ≤ 37 / 40 * Real.log t

For t ≥ 2, Uρ t ≤ (37/40) log t (total mass of ρ is 37/40).

theorem Zeta5Irrational.Vfield_ge_tail {t : ℝ} (ht : 2 ≤ t) : 2 * Real.pi * √t + Real.log t - 6 * (3 / 40) * (Real.log t + (3 / 40) ^ 2 / t) ≤ Vfield t

The lower bound for V used in (6.8): V(t) ≥ 2π√t + log t - 6α (log t + α²/t).

theorem Zeta5Irrational.potential_ineq_tail {t : ℝ} (ht : 2 ≤ t) : 2 * Uρ t - Vfield t ≤ M0

The tail t ≥ 2 of the potential inequality (6.2), via (6.8).