The antipodal floor of moment power series on the unit circle, and |Li_s| ≥ η(s)

For a finite measure μ and a function τ with values in [0, 1) almost everywhere, the power series of the moments q_k = ∫ τ^k dμ, wherever it converges on the unit circle (at every z ≠ 1, by Dirichlet's test), has modulus at least ∫ 1/(1 + τ) dμ, which is the sum of the alternating series of the moments. With the measure x^(s−1) e^(−x)/Γ(s) dx and τ = e^(−x), the moments are (k+1)^(−s): for every real s > 0 and every z ≠ 1 on the unit circle, the polylogarithm series converges and its sum has modulus at least η(s), with equality at z = −1. The polylogarithm is handled through its partial sums (partialLi), because for s ≤ 1 the convergence on the circle is only conditional. Classical mathematics: a consequence of Fejér's theorem on four times monotone coefficients (Acta Sci. Math. Szeged 8 (1937), p. 104); for s = 2 stated in Boyer–Parry, arXiv:2111.12226, Appendix A, Lemma 8. Generalises Dilog.antipode_floor (finite mixtures of geometric populations).

Main results

• Polylog.one_div_one_add_le_re: Re(1/(1 − xz)) ≥ 1/(1 + x) for x ∈ [0, 1), |z| = 1
• Polylog.le_norm_of_tendsto: the moment series, if it converges at |z| = 1, has modulus ≥ ∫ 1/(1 + τ) dμ
• Polylog.tendsto_alternating: the alternating series of the moments sums to ∫ 1/(1 + τ) dμ
• Polylog.exists_tendsto_circle: the moment series converges at every z ≠ 1 of the unit circle
• Polylog.exists_tendsto_eta: η(s) converges to a positive number for s > 0
• Polylog.exists_tendsto_partialLi: the series of Li_s converges at every z ≠ 1 of the unit circle, s > 0
• Polylog.polylog_circle_floor: η(s) ≤ |Li_s z| on the unit circle, s > 0, z ≠ 1
• Polylog.polylog_neg_one: Li_s(−1) = −η(s): the floor is attained

References

• C. Marín, The Clock That Never Ticks: a machine-checked path from the dilogarithm to quantum speed limits in Lean 4, Zenodo (2026), doi:10.5281/zenodo.20675271, thm:clock.

theorem Polylog.one_div_one_add_le_re {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) {z : ℂ} (hz : ‖z‖ = 1) : 1 / (1 + x) ≤ (1 / (1 - ↑x * z)).re

The per-term bound. For x ∈ [0, 1) and z on the unit circle, 1 / (1 + x) ≤ Re (1 / (1 - x z)); the gap is x (1 - x) (1 + Re z) / ((1 + x) |1 - x z|²).

noncomputable def Polylog.moment {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (τ : α → ℝ) (k : ℕ) : ℝ

The moments ∫ τ ^ k ∂μ.

Equations

• Polylog.moment μ τ k = ∫ (a : α), τ a ^ k ∂μ

theorem Polylog.integrable_pow_aux {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (τ : α → ℝ) [MeasureTheory.IsFiniteMeasure μ] (hτm : Measurable τ) (hτ0 : ∀ᵐ (a : α) ∂μ, 0 ≤ τ a) (hτ1 : ∀ᵐ (a : α) ∂μ, τ a < 1) (k : ℕ) : MeasureTheory.Integrable (fun (a : α) => τ a ^ k) μ

Auxiliary: τ ^ k is integrable when 0 ≤ τ < 1 a.e.

theorem Polylog.integrable_inv_aux {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (τ : α → ℝ) (hτm : Measurable τ) (hτ0 : ∀ᵐ (a : α) ∂μ, 0 ≤ τ a) {r : ℝ} (hr : 0 ≤ r) : MeasureTheory.Integrable (fun (a : α) => 1 / (1 + τ a * r)) μ

Auxiliary: bounded measurable functions are integrable (version for 1 / (1 + τ r)).

theorem Polylog.tendsto_moment_zero {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (τ : α → ℝ) (hτm : Measurable τ) (hτ0 : ∀ᵐ (a : α) ∂μ, 0 ≤ τ a) (hτ1 : ∀ᵐ (a : α) ∂μ, τ a < 1) : Filter.Tendsto (moment μ τ) Filter.atTop (nhds 0)

Auxiliary: the moments tend to 0.

theorem Polylog.le_norm_of_tendsto {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (τ : α → ℝ) (hτm : Measurable τ) (hτ0 : ∀ᵐ (a : α) ∂μ, 0 ≤ τ a) (hτ1 : ∀ᵐ (a : α) ∂μ, τ a < 1) {z : ℂ} (hz : ‖z‖ = 1) {F : ℂ} (hF : Filter.Tendsto (fun (N : ℕ) => ∑ k ∈ Finset.range N, ↑(moment μ τ k) * z ^ k) Filter.atTop (nhds F)) : ∫ (a : α), 1 / (1 + τ a) ∂μ ≤ ‖F‖

The antipodal floor. If the moment series converges at a point z of the unit circle, its sum has modulus at least ∫ 1 / (1 + τ) ∂μ.

theorem Polylog.tendsto_alternating {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (τ : α → ℝ) (hτm : Measurable τ) (hτ0 : ∀ᵐ (a : α) ∂μ, 0 ≤ τ a) (hτ1 : ∀ᵐ (a : α) ∂μ, τ a < 1) : Filter.Tendsto (fun (N : ℕ) => ∑ k ∈ Finset.range N, (-1) ^ k * moment μ τ k) Filter.atTop (nhds (∫ (a : α), 1 / (1 + τ a) ∂μ))

The alternating series of the moments sums to ∫ 1 / (1 + τ) ∂μ: the floor is the value of the series at z = -1.

theorem Polylog.exists_tendsto_circle {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (τ : α → ℝ) (hτm : Measurable τ) (hτ0 : ∀ᵐ (a : α) ∂μ, 0 ≤ τ a) (hτ1 : ∀ᵐ (a : α) ∂μ, τ a < 1) {z : ℂ} (hz : ‖z‖ = 1) (hz1 : z ≠ 1) : ∃ (F : ℂ), Filter.Tendsto (fun (N : ℕ) => ∑ k ∈ Finset.range N, ↑(moment μ τ k) * z ^ k) Filter.atTop (nhds F)

The moment series converges at every point z ≠ 1 of the unit circle (Dirichlet's test: the moments decrease to 0).

noncomputable def Polylog.partialLi (s : ℝ) (z : ℂ) (N : ℕ) : ℂ

The partial sums of the polylogarithm series ∑_{n ≥ 1} z ^ n / n ^ s.

Equations

• Polylog.partialLi s z N = ∑ k ∈ Finset.range N, z ^ (k + 1) / ↑((↑k + 1) ^ s)

noncomputable def Polylog.partialEta (s : ℝ) (N : ℕ) : ℝ

The partial sums of η(s) = ∑_{n ≥ 1} (-1) ^ (n - 1) / n ^ s.

Equations

• Polylog.partialEta s N = ∑ k ∈ Finset.range N, (-1) ^ k / (↑k + 1) ^ s

theorem Polylog.exists_tendsto_eta {s : ℝ} (hs : 0 < s) : ∃ (e : ℝ), Filter.Tendsto (partialEta s) Filter.atTop (nhds e) ∧ 0 < e

η(s) converges for s > 0, to a positive number.

theorem Polylog.polylog_neg_one {s e : ℝ} (he : Filter.Tendsto (partialEta s) Filter.atTop (nhds e)) : Filter.Tendsto (partialLi s (-1)) Filter.atTop (nhds (-↑e))

The floor is attained at z = -1: there Li_s (-1) = -η(s).

The Gamma measure

noncomputable def Polylog.gammaMeasure (s : ℝ) : MeasureTheory.Measure ℝ

The measure x ^ (s - 1) e ^ (-x) / Γ(s) dx on (0, ∞).

Equations

• Polylog.gammaMeasure s = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (x : ℝ) => ENNReal.ofReal (Real.exp (-x) * x ^ (s - 1) / Real.Gamma s)

theorem Polylog.gammaMeasure_univ {s : ℝ} (hs : 0 < s) : (gammaMeasure s) Set.univ = 1

theorem Polylog.gammaMeasure_isFinite {s : ℝ} (hs : 0 < s) : MeasureTheory.IsFiniteMeasure (gammaMeasure s)

theorem Polylog.gamma_ae {s : ℝ} (p : ℝ → Prop) (hp : ∀ (x : ℝ), 0 < x → p x) : ∀ᵐ (x : ℝ) ∂gammaMeasure s, p x

theorem Polylog.gamma_moment {s : ℝ} (hs : 0 < s) (k : ℕ) : moment (gammaMeasure s) (fun (x : ℝ) => Real.exp (-x)) k = ((↑k + 1) ^ s)⁻¹

theorem Polylog.gamma_hli {s : ℝ} (hs : 0 < s) {z : ℂ} (hz : ‖z‖ = 1) (N : ℕ) : z⁻¹ * partialLi s z N = ∑ k ∈ Finset.range N, ↑(moment (gammaMeasure s) (fun (x : ℝ) => Real.exp (-x)) k) * z ^ k

theorem Polylog.gamma_eta {s : ℝ} (hs : 0 < s) (N : ℕ) : partialEta s N = ∑ k ∈ Finset.range N, (-1) ^ k * moment (gammaMeasure s) (fun (x : ℝ) => Real.exp (-x)) k

theorem Polylog.exists_tendsto_partialLi {s : ℝ} (hs : 0 < s) {z : ℂ} (hz : ‖z‖ = 1) (hz1 : z ≠ 1) : ∃ (L : ℂ), Filter.Tendsto (partialLi s z) Filter.atTop (nhds L)

The polylogarithm series converges at every z ≠ 1 of the unit circle, for s > 0.

theorem Polylog.polylog_circle_floor {s : ℝ} (hs : 0 < s) {z : ℂ} (hz : ‖z‖ = 1) {L : ℂ} (hL : Filter.Tendsto (partialLi s z) Filter.atTop (nhds L)) {e : ℝ} (he : Filter.Tendsto (partialEta s) Filter.atTop (nhds e)) : e ≤ ‖L‖

The floor of the polylogarithm on the unit circle. For real s > 0 and z ≠ 1 on the unit circle, η(s) ≤ |Li_s z|.