The complex dilogarithm on the closed unit disk

The complex dilogarithm Li₂c z = ∑_{n ≥ 1} zⁿ / n² on ‖z‖ ≤ 1, its boundary values, and a first step toward O'Sullivan's localization of the zeros of the branches φ_{A,B}(z) = Li₂c z + 4π² A + 2π i B log z.

Main definitions

• Dilog.Li₂c: the complex dilogarithm.
• Dilog.phi A B: the branch Li₂c z + 4π² A + 2π i B log z.
• Dilog.Iθ B θ r: the imaginary part of φ_{0,B}(r e^{iθ}).

Main results

• Dilog.Li₂c_exp_re, Dilog.Li₂c_exp_im: on the unit circle Re Li₂c(e^{iθ}) = π²/6 - πθ/2 + θ²/4 and Im Li₂c(e^{iθ}) = Cl₂ θ (O'Sullivan (2.8)–(2.9)).
• Dilog.Li₂c_exp_ne_zero: Li₂c (e^{iθ}) ≠ 0 for θ ∈ (0, 2π).
• Dilog.hasDerivAt_Li₂c, Dilog.hasDerivAt_phi: derivatives inside the disk.
• Dilog.exists_Iθ_zero_lt_one: for B ≥ 1 and θ ∈ (0, π), Iθ B θ vanishes at some radius r ∈ (0, 1).
• Dilog.Li₂c_I: Li₂(i) = -π²/48 + i G.
• Dilog.Li₂c_two_pi_mul: Li₂c(e^{2πix}) = π² B₂(x) + i Cl₂(2πx) for x ∈ [0, 1].

References

• C. O'Sullivan, Zeros of the dilogarithm, Math. Comp. 85 (2016) 2967–2993.

noncomputable def Dilog.Li₂c (z : ℂ) : ℂ

The complex dilogarithm ∑_{n≥1} zⁿ/n², convergent on the closed unit disk.

Equations

• Dilog.Li₂c z = ∑' (n : ℕ), z ^ (n + 1) / (↑n + 1) ^ 2

theorem Dilog.summable_Li₂c {z : ℂ} (hz : ‖z‖ ≤ 1) : Summable fun (n : ℕ) => z ^ (n + 1) / (↑n + 1) ^ 2

The defining series of Li₂c is absolutely summable on the closed unit disk.

theorem Dilog.Li₂c_exp_re_eq (θ : ℝ) : (Li₂c (Complex.exp (↑θ * Complex.I))).re = zetaStateRe θ

The real part on the unit circle equals zetaStateRe (from Clausen).

theorem Dilog.Li₂c_exp_im (θ : ℝ) : (Li₂c (Complex.exp (↑θ * Complex.I))).im = Cl₂ θ

The imaginary part on the unit circle equals Cl₂ (O'Sullivan (2.9)).

theorem Dilog.zetaStateRe_eq {θ : ℝ} (h0 : 0 ≤ θ) (h2π : θ ≤ 2 * Real.pi) : zetaStateRe θ = Real.pi ^ 2 / 6 - Real.pi * θ / 2 + θ ^ 2 / 4

The Bernoulli parabola, for the (n+1)-indexed sum (general θ); generalizes zetaStateRe_pi to all θ ∈ [0, 2π].

theorem Dilog.Li₂c_exp_re {θ : ℝ} (h0 : 0 ≤ θ) (h2π : θ ≤ 2 * Real.pi) : (Li₂c (Complex.exp (↑θ * Complex.I))).re = Real.pi ^ 2 / 6 - Real.pi * θ / 2 + θ ^ 2 / 4

Real part on the unit circle: the Bernoulli parabola (O'Sullivan (2.8)).

theorem Dilog.hasDerivAt_Li₂c {z : ℂ} (hz : ‖z‖ < 1) (hz0 : z ≠ 0) : HasDerivAt Li₂c (-Complex.log (1 - z) / z) z

The analytic core, complex form: Li₂c'(z) = -log(1-z)/z on the punctured open disk. The complex companion of Dilog.hasDerivAt_Li₂, by the same term-by-term differentiation under a geometric majorant on a ball, then the complex Mercator series.

theorem Dilog.Li₂c_exp_ne_zero {θ : ℝ} (h0 : 0 < θ) (h2π : θ < 2 * Real.pi) : Li₂c (Complex.exp (↑θ * Complex.I)) ≠ 0

No zero on the unit circle for θ ∈ (0, 2π) (principal branch). Direct from zetaState_never_orthogonal via the boundary decomposition.

noncomputable def Dilog.phi (A B : ℤ) (z : ℂ) : ℂ

The multivalued dilogarithm branch φ_{A,B}(z) = Li₂(z) + 4π²A + 2πiB·log z (O'Sullivan, A,B ∈ ℤ). On the principal branch A = B = 0, φ = Li₂c.

Equations

• Dilog.phi A B z = Dilog.Li₂c z + 4 * ↑Real.pi ^ 2 * ↑A + 2 * ↑Real.pi * Complex.I * ↑B * Complex.log z

theorem Dilog.hasDerivAt_phi (A B : ℤ) {z : ℂ} (hz : ‖z‖ < 1) (hslit : z ∈ Complex.slitPlane) : HasDerivAt (phi A B) (-Complex.log (1 - z) / z + 2 * ↑Real.pi * Complex.I * ↑B * z⁻¹) z

The derivative of φ_{A,B} on the punctured slit disk.

theorem Dilog.z_mul_deriv_phi (B : ℤ) {z : ℂ} (hslit : z ∈ Complex.slitPlane) : z * (-Complex.log (1 - z) / z + 2 * ↑Real.pi * Complex.I * ↑B * z⁻¹) = -Complex.log (1 - z) + 2 * ↑Real.pi * Complex.I * ↑B

O'Sullivan (2.1): z·φ'_{A,B}(z) = -log(1-z) + 2πiB on the punctured slit disk.

theorem Dilog.continuousOn_Li₂c : ContinuousOn Li₂c (Metric.closedBall 0 1)

Li₂c is continuous on the closed unit disk (Weierstrass M-test).

Phase 3: sign localization of the imaginary-part zero curve (O'Sullivan §5)

For B ≥ 1, the zero w(A,B) of φ_{A,B} lies on the curve Im φ_{A,B} = 0. Along the ray z = r·e^{iθ} this imaginary part is I_θ(r) = Im Li₂(r e^{iθ}) + 2πB·log r (O'Sullivan (5.2), since Re log z = log r). At the unit circle r = 1 it reduces to Cl₂(θ); its sign (via our Cl₂_pos) decides whether the zero sits inside (Cl₂ > 0) or outside the disk — the seed of O'Sullivan's Proposition 5.3.

noncomputable def Dilog.Iθ (B : ℤ) (θ r : ℝ) : ℝ

The imaginary part of φ_{0,B} along the ray r·e^{iθ} (O'Sullivan (5.2)).

Equations

• Dilog.Iθ B θ r = (Dilog.Li₂c (↑r * Complex.exp (↑θ * Complex.I))).im + 2 * Real.pi * ↑B * Real.log r

theorem Dilog.Iθ_one (B : ℤ) (θ : ℝ) : Iθ B θ 1 = Cl₂ θ

O'Sullivan §5, the key identity: at the unit circle I_θ(1) = Cl₂(θ).

theorem Dilog.Iθ_one_pos (B : ℤ) {θ : ℝ} (h0 : 0 < θ) (hπ : θ < Real.pi) : 0 < Iθ B θ 1

On the arc θ ∈ (0,π) the imaginary-part function is positive at the unit circle — the sign that localizes the zero inside the disk (O'Sullivan Prop. 5.3).

theorem Dilog.norm_Li₂c_le {z : ℂ} (hz : ‖z‖ ≤ 1) : ‖Li₂c z‖ ≤ ∑' (n : ℕ), ‖1 / (↑n + ↑1) ^ 2‖

A uniform bound ‖Li₂c z‖ ≤ M on the closed disk, M = ∑ ‖1/(n+1)²‖.

theorem Dilog.exists_Iθ_zero_lt_one (B : ℤ) (hB : 1 ≤ B) {θ : ℝ} (h0 : 0 < θ) (hπ : θ < Real.pi) : ∃ r ∈ Set.Ioo 0 1, Iθ B θ r = 0

O'Sullivan Prop. 5.3 (localization, the achievable core): for B ≥ 1 and θ ∈ (0,π), the imaginary-part curve I_θ = 0 is met strictly inside the unit disk. Proof: I_θ(1) = Cl₂(θ) > 0, I_θ is ≤ 0 at a small r₀ ∈ (0,1) (the 2πB·log r term dominates the bounded Im Li₂c), and continuity + the intermediate value theorem.

Phase 4: the B₂/Cl₂ decomposition at roots of unity (O'Sullivan (2.8)+(2.9))

The seed of the asymptotic zero location (O'Sullivan Thm 7.3): the value of the dilogarithm at a root of unity splits into the second Bernoulli polynomial (real part) and the Clausen function (imaginary part).

noncomputable def Dilog.B₂ (x : ℝ) : ℝ

The second Bernoulli polynomial B₂(x) = x² − x + 1/6.

Equations

• Dilog.B₂ x = x ^ 2 - x + 1 / 6

theorem Dilog.Li₂c_two_pi_mul {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : Li₂c (Complex.exp (↑(2 * Real.pi * x) * Complex.I)) = ↑(Real.pi ^ 2 * B₂ x) + ↑(Cl₂ (2 * Real.pi * x)) * Complex.I

O'Sullivan (2.8)+(2.9): at a root of unity e^{2πix} (x ∈ [0,1]), Li₂(e^{2πix}) = π²·B₂(x) + i·Cl₂(2πx). This B₂/Cl₂ decomposition is the first-order content of the zero-location asymptotic (Thm 7.3) and the bridge to Rademacher's partition asymptotics.

theorem Dilog.Li₂c_I : Li₂c Complex.I = ↑(-Real.pi ^ 2 / 48) + ↑catalanConst * Complex.I

Li₂(i) = −π²/48 + i G: the parabola and Catalan's constant at the quarter circle.