The Clausen function and Catalan's constant

The Clausen function Cl₂ θ = ∑_{n ≥ 1} sin(nθ) / n² is the imaginary part of the dilogarithm on the unit circle. Its real part is the Bernoulli parabola ∑ cos(nθ)/n² = π²/6 - πθ/2 + θ²/4 on [0, 2π], derived here from Mathlib's Fourier expansion of the Bernoulli polynomials. Abel summation and the Fejér–Jackson inequality give Cl₂ θ > 0 on (0, π).

Main definitions

• Dilog.Cl₂: the Clausen function.
• Dilog.catalanConst: Catalan's constant G = ∑ (-1)^k / (2k + 1)².
• Dilog.zetaStateRe: the cosine series ∑ cos(nθ) / n².

Main results

• Dilog.Cl₂_neg, Dilog.Cl₂_two_pi_sub: symmetries.
• Dilog.Cl₂_pi_div_two: Cl₂ (π/2) = G.
• Dilog.Cl₂_two_mul: duplication Cl₂(2θ) = 2 Cl₂(θ) - 2 Cl₂(π - θ); Dilog.Cl₂_two_pi_div_three.
• Dilog.hasSum_cos_div_sq: the Bernoulli parabola.
• Dilog.Cl₂_pos: 0 < Cl₂ θ for θ ∈ (0, π).
• Dilog.zetaState_never_orthogonal: for θ ∈ (0, 2π) the two series ∑ cos(nθ)/n² and ∑ sin(nθ)/n² do not vanish together.
• Dilog.zetaState_meanEnergy_not_summable, Dilog.zetaState_secondMoment_not_summable: the populations 6/(π² n²) on the levels n have infinite mean energy and infinite second moment.

References

• L. Lewin, Polylogarithms and Associated Functions, North-Holland, 1981, Chapter 4.

noncomputable def Dilog.Cl₂ (θ : ℝ) : ℝ

The Clausen function Cl₂(θ) = ∑_{n≥1} sin(nθ)/n², the imaginary part of the dilogarithm on the unit circle.

Equations

• Dilog.Cl₂ θ = ∑' (n : ℕ), Real.sin ((↑n + 1) * θ) / (↑n + 1) ^ 2

theorem Dilog.summable_Cl₂ (θ : ℝ) : Summable fun (n : ℕ) => Real.sin ((↑n + 1) * θ) / (↑n + 1) ^ 2

The Clausen series converges absolutely (dominated by ∑ 1/(n+1)²).

@[simp]

theorem Dilog.Cl₂_zero : Cl₂ 0 = 0

@[simp]

theorem Dilog.Cl₂_pi : Cl₂ Real.pi = 0

Cl₂(π) = 0 — every term sin((n+1)π) vanishes.

theorem Dilog.Cl₂_neg (θ : ℝ) : Cl₂ (-θ) = -Cl₂ θ

Cl₂ is an odd function.

noncomputable def Dilog.catalanConst : ℝ

Catalan's constant G = ∑_{k≥0} (−1)^k/(2k+1)² = 0.9159… — the value of the Dirichlet beta function at 2. Its irrationality is a famous open problem.

Equations

• Dilog.catalanConst = ∑' (k : ℕ), (-1) ^ k / (2 * ↑k + 1) ^ 2

theorem Dilog.summable_catalanConst : Summable fun (k : ℕ) => (-1) ^ k / (2 * ↑k + 1) ^ 2

The defining series of Catalan's constant converges absolutely.

theorem Dilog.Cl₂_pi_div_two : Cl₂ (Real.pi / 2) = catalanConst

Cl₂(π/2) = G — Catalan's constant is the Clausen function at the quarter circle. (Even-indexed sines vanish, odd-indexed give the alternating series.)

theorem Dilog.hasSum_cos_div_sq {θ : ℝ} (h0 : 0 ≤ θ) (h2π : θ ≤ 2 * Real.pi) : HasSum (fun (n : ℕ) => Real.cos (↑n * θ) / ↑n ^ 2) (Real.pi ^ 2 / 6 - Real.pi * θ / 2 + θ ^ 2 / 4)

The Bernoulli parabola: for θ ∈ [0, 2π], ∑_{n≥1} cos(nθ)/n² = π²/6 − πθ/2 + θ²/4 — the real part of Li₂ on the unit circle (the weight-2 Fourier expansion of the Bernoulli polynomial B₂). Note the n = 0 term of the ℕ-indexed sum is 0 by the 1/0 = 0 convention.

Positivity of Cl₂ on (0, π)

Abel rearrangement of the partial sums of the Cl₂ series in terms of the Fejér–Jackson sums, then fejerSum_pos makes every piece positive. The arrangement is asymptotics-free: every partial sum is at least sin θ / 2.

theorem Dilog.sin_div_two_le_Cl₂ {θ : ℝ} (h0 : 0 < θ) (hπ : θ < Real.pi) : Real.sin θ / 2 ≤ Cl₂ θ

The asymptotics-free Clausen bound on (0, π): Cl₂ θ ≥ sin θ / 2. Abel summation writes each partial sum through the Fejér–Jackson sums, all positive, and the first term alone is sin θ / 2.

theorem Dilog.Cl₂_pos {θ : ℝ} (h0 : 0 < θ) (hπ : θ < Real.pi) : 0 < Cl₂ θ

Positivity of the Clausen function on (0, π): 0 < Cl₂ θ, from Cl₂ θ ≥ sin θ / 2; the analytic heart of "weight-2 zeta states never reach an orthogonal state".

The clock that never ticks

The weight-2 zeta state — populations ∝ 1/n² on equally spaced energy levels — has autocorrelation S(θ) = (6/π²)·Li₂(e^{−iθ}), with real part zetaStateRe (the Bernoulli parabola) and imaginary part −Cl₂. Despite infinite mean energy and infinite energy variance (so the Margolus–Levitin and Mandelstam–Tamm bounds say nothing), the state never reaches an orthogonal state: S has no zero on (0, 2π).

theorem Dilog.Cl₂_two_pi_sub (θ : ℝ) : Cl₂ (2 * Real.pi - θ) = -Cl₂ θ

Reflection at the full circle: Cl₂(2π − θ) = −Cl₂(θ).

noncomputable def Dilog.zetaStateRe (θ : ℝ) : ℝ

The real part of the weight-2 zeta-state autocorrelation, ∑ cos(nθ)/n² (indexed like Cl₂).

Equations

• Dilog.zetaStateRe θ = ∑' (n : ℕ), Real.cos ((↑n + 1) * θ) / (↑n + 1) ^ 2

theorem Dilog.zetaStateRe_pi : zetaStateRe Real.pi = -Real.pi ^ 2 / 12

At the antipode θ = π the real part is −π²/12 ≠ 0 (Bernoulli parabola).

theorem Dilog.zetaState_never_orthogonal {θ : ℝ} (h0 : 0 < θ) (h2π : θ < 2 * Real.pi) : ¬(zetaStateRe θ = 0 ∧ Cl₂ θ = 0)

The clock that never ticks: the weight-2 zeta-state autocorrelation never vanishes on (0, 2π) — its real part (zetaStateRe) and imaginary part (−Cl₂) are never simultaneously zero. The quantum state with populations ∝ 1/n² on equally spaced levels has infinite mean energy, yet never reaches an orthogonal state.

theorem Dilog.zetaState_meanEnergy_not_summable : ¬Summable fun (n : ℕ) => 6 / (Real.pi ^ 2 * (↑n + 1) ^ 2) * (↑n + 1)

The weight-2 zeta state has infinite mean energy: ∑ₙ pₙ Eₙ with pₙ = 6/(π² n²) and Eₙ = n is the harmonic series up to the factor 6/π².

theorem Dilog.zetaState_secondMoment_not_summable : ¬Summable fun (n : ℕ) => 6 / (Real.pi ^ 2 * (↑n + 1) ^ 2) * (↑n + 1) ^ 2

The weight-2 zeta state has infinite second moment ∑ₙ pₙ Eₙ², so its energy variance is infinite too.

theorem Dilog.Cl₂_two_mul (θ : ℝ) : Cl₂ (2 * θ) = 2 * Cl₂ θ - 2 * Cl₂ (Real.pi - θ)

Duplication of the Clausen function: Cl₂(2θ) = 2 Cl₂(θ) − 2 Cl₂(π − θ), the circle shadow of Li₂(z²) = 2(Li₂ z + Li₂(−z)) (even indices survive, odd ones cancel).

theorem Dilog.Cl₂_two_pi_div_three : Cl₂ (2 * Real.pi / 3) = 2 / 3 * Cl₂ (Real.pi / 3)

Cl₂(2π/3) = (2/3) Cl₂(π/3): duplication at θ = π/3.