The integral of log x / x

(log x)² / 2 is an antiderivative of log x / x on (0, ∞), so ∫₁ᴺ log x / x dx = (log N)² / 2 for N ≥ 1.

This is the integral behind the corrected heat-capacity coefficient (log N)² / 12 at the Hagedorn point (see Formalizations.Analysis.TransformerAttention.HeatCapacity).

Main results

• Real.hasDerivAt_log_sq_div_two: d/dx [(log x)² / 2] = log x / x for x > 0.
• integral_log_div_self: ∫ x in 1..N, log x / x = (log N)² / 2 for 1 ≤ N.

References

• C. Marín, Predicting How Transformers Attend (2026), §5.2 and its erratum, Zenodo 19826343. Ported from Taf/CvHagedornCorrection.lean of karlesmarin/lean-taf (Lean v4.30.0-rc2).

Related

Mathlib has integral_log, integral_inv and integral_inv_div_log in Mathlib.Analysis.SpecialFunctions.Integrals.Basic, but not this integral, neither at the pinned commit nor in current Mathlib (checked with Loogle, LeanSearch and GitHub code search, October 2026).

theorem Real.hasDerivAt_log_sq_div_two {x : ℝ} (hx : 0 < x) : HasDerivAt (fun (y : ℝ) => log y ^ 2 / 2) (log x / x) x

d/dx [(log x)² / 2] = log x / x for x > 0.

theorem integral_log_div_self (N : ℝ) (hN : 1 ≤ N) : ∫ (x : ℝ) in 1..N, Real.log x / x = Real.log N ^ 2 / 2

∫₁ᴺ log x / x dx = (log N)² / 2 for N ≥ 1.