The dilogarithm stays away from zero on the unit circle

On the unit circle ‖Li₂ z‖ ≥ π²/12 = |Li₂(−1)|: the minimum modulus sits at the antipode. Hence the weight-2 zeta state (populations 6/(π² n²) on the levels n) never gets halfway to an orthogonal state, |S(θ)| ≥ 1/2 for every θ.

The proof writes Li₂(w) = w ∫∫_{(0,1)²} dx dy / (1 − xyw) on the open disk (the moments ∫∫ (xy)ⁿ = 1/(n+1)² and a sum–integral exchange), bounds each mode by Re (1 − tz)⁻¹ ≥ (1 + t)⁻¹ for t ∈ [0,1), ‖z‖ = 1, which gives ‖Li₂(rz)‖ ≥ −Li₂(−r) for r < 1, and lets r → 1⁻ by continuity of Li₂ on the closed disk.

Main results

• Dilog.Li₂c_eq_mul_integral: the integral representation on the open unit disk.
• Dilog.inv_one_add_le_re_inv: the per-mode floor.
• Dilog.norm_Li₂c_ge: π²/12 ≤ ‖Li₂c z‖ for ‖z‖ = 1.
• Dilog.zetaState_norm_ge_half: 1/2 ≤ (6/π²) ‖Li₂c (e^{iθ})‖.

def Dilog.unitSq : Set (ℝ × ℝ)

The open unit square.

Equations

• Dilog.unitSq = Set.Ioo 0 1 ×ˢ Set.Ioo 0 1

theorem Dilog.measurableSet_unitSq : MeasurableSet unitSq

theorem Dilog.volume_unitSq_ne_top : MeasureTheory.volume unitSq ≠ ⊤

instance Dilog.instIsFiniteMeasureProdRealRestrictVolumeUnitSq : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitSq)

theorem Dilog.mem_unitSq {p : ℝ × ℝ} (hp : p ∈ unitSq) : 0 < p.1 * p.2 ∧ p.1 * p.2 < 1

theorem Dilog.integral_mul_pow_unitSq (n : ℕ) : ∫ (p : ℝ × ℝ) in unitSq, (p.1 * p.2) ^ n = 1 / (↑n + 1) ^ 2

∫∫_{(0,1)²} (xy)ⁿ = 1/(n+1)².

theorem Dilog.inv_one_add_le_re_inv {t : ℝ} (h0 : 0 ≤ t) (h1 : t < 1) {z : ℂ} (hz : ‖z‖ = 1) : (1 + t)⁻¹ ≤ (1 - ↑t * z)⁻¹.re

The per-mode floor: for t ∈ [0, 1) and ‖z‖ = 1, Re (1 - t z)⁻¹ ≥ (1 + t)⁻¹.

theorem Dilog.norm_inv_one_sub_le {q : ℝ} (h0 : 0 < q) (h1 : q < 1) {w : ℂ} (hw : ‖w‖ < 1) : ‖(1 - ↑q * w)⁻¹‖ ≤ (1 - ‖w‖)⁻¹

‖(1 - q w)⁻¹‖ ≤ (1 - ‖w‖)⁻¹ for q ∈ (0, 1) and ‖w‖ < 1.

theorem Dilog.aestronglyMeasurable_inv_one_sub (w : ℂ) : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × ℝ) => (1 - ↑(p.1 * p.2) * w)⁻¹) (MeasureTheory.volume.restrict unitSq)

theorem Dilog.Li₂c_eq_mul_integral {w : ℂ} (hw : ‖w‖ < 1) : Li₂c w = w * ∫ (p : ℝ × ℝ) in unitSq, (1 - ↑(p.1 * p.2) * w)⁻¹

Li₂(w) = w ∫∫_{(0,1)²} dx dy / (1 - xyw) on the open unit disk.

theorem Dilog.Li₂c_ofReal (x : ℝ) : Li₂c ↑x = ↑(Li₂ x)

theorem Dilog.neg_Li₂_neg_eq {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) : -Li₂ (-r) = r * ∫ (p : ℝ × ℝ) in unitSq, (1 + p.1 * p.2 * r)⁻¹

theorem Dilog.floor_of_lt_one {r : ℝ} (hr0 : 0 < r) (hr1 : r < 1) {z : ℂ} (hz : ‖z‖ = 1) : -Li₂ (-r) ≤ ‖Li₂c (↑r * z)‖

theorem Dilog.norm_Li₂c_ge {z : ℂ} (hz : ‖z‖ = 1) : Real.pi ^ 2 / 12 ≤ ‖Li₂c z‖

The antipode floor for the dilogarithm: on the unit circle ‖Li₂ z‖ ≥ π²/12 = |Li₂(−1)|.

theorem Dilog.zetaState_norm_ge_half (θ : ℝ) : 1 / 2 ≤ 6 / Real.pi ^ 2 * ‖Li₂c (Complex.exp (↑θ * Complex.I))‖

The weight-2 zeta state never gets halfway to an orthogonal state: |S(θ)| ≥ 1/2 for every θ, with S(θ) = (6/π²) Li₂(e^{iθ}) (the paper's Figure 3, there certified numerically).