The closed form (A.5) of the external field V

∫₀^c log(t + u²) du = c log(t + c²) - 2c + 2√t arctan(c/√t) for t > 0, hence V(t) = log(1+t) - 6α log(t+α²) - 2 + 12α + 2√t (π + arctan(1/√t) - 6 arctan(α/√t)).

noncomputable def Zeta5Irrational.GVpot (t u : ℝ) : ℝ

Antiderivative of u ↦ log (t + u²).

Equations

• Zeta5Irrational.GVpot t u = u * Real.log (t + u ^ 2) - 2 * u + 2 * √t * Real.arctan (u / √t)

theorem Zeta5Irrational.hasDerivAt_GV {t : ℝ} (ht : 0 < t) (u : ℝ) : HasDerivAt (GVpot t) (Real.log (t + u ^ 2)) u

theorem Zeta5Irrational.integral_log_add_sq {t : ℝ} (ht : 0 < t) (c : ℝ) : ∫ (u : ℝ) in 0..c, Real.log (t + u ^ 2) = c * Real.log (t + c ^ 2) - 2 * c + 2 * √t * Real.arctan (c / √t)

∫₀^c log(t + u²) du = c log(t + c²) - 2c + 2√t arctan(c/√t) for t > 0.

theorem Zeta5Irrational.Vfield_eq {t : ℝ} (ht : 0 < t) : Vfield t = Real.log (1 + t) - 6 * (3 / 40) * Real.log (t + (3 / 40) ^ 2) - 2 + 12 * (3 / 40) + 2 * √t * (Real.pi + Real.arctan (1 / √t) - 6 * Real.arctan (3 / 40 / √t))

(A.5): the closed form of V.