The complex dilogarithm #

Complex counterparts of LeanPool.PolylogIntegrals.Lemmas.Dilog for the series LeanPolyLog.Li, and Landen's identity on the closed unit disk.

Main results #

LeanPolyLog.Dilog.Li_one: Li_1(z) = -log(1 - z) on the open unit disk.
LeanPolyLog.Dilog.ofReal_Lir: Lir s x = Li s x for real x.
LeanPolyLog.Dilog.continuousOn_Li: for s ≥ 2, Li_s is continuous on the closed unit disk.
LeanPolyLog.Dilog.hasDerivAt_Li_succ, LeanPolyLog.Dilog.hasDerivAt_Li_two: for 0 < ‖z‖ < 1, Li_(s+1)'(z) = Li_s(z)/z; in particular Li_2'(z) = -log(1 - z)/z.
LeanPolyLog.Dilog.Li_sq: the duplication formula Li_s(z²) = 2^(s-1) (Li_s(z) + Li_s(-z)).
LeanPolyLog.Dilog.eq_of_hasDerivAt_eq_zero_complex: a function ℝ → ℂ that is continuous on [a, b] with derivative 0 on (a, b) has f a = f b.
LeanPolyLog.Dilog.Li_two_add_Li_two_div_sub_one: Landen's identity Li_2(z) + Li_2(z/(z-1)) = -½ log²(1 - z) for ‖z‖ ≤ 1 and Re z ≤ 1/2.
LeanPolyLog.Dilog.log_one_sub_I: log(1 - i) = ½ log 2 - (π/4) i.

Proof sketch #

Landen's identity is proved along the segment t ↦ tz, t ∈ [0, 1]. The condition Re z ≤ 1/2 gives ‖tz‖ ≤ ‖tz - 1‖, so tz/(tz - 1) stays in the closed unit disk, and 1 - tz stays in the right half-plane, where the principal log is holomorphic and log (1 - tz)⁻¹ = -log (1 - tz). The function Li_2(tz) + Li_2(tz/(tz-1)) + ½ log²(1 - tz) is therefore continuous on [0, 1], has derivative 0 on (0, 1) and vanishes at t = 0.

The complex polylogarithm `Li` #

source

@[simp]

theorem LeanPolyLog.Dilog.Li_zero (s : ℕ) :

Li s 0 = 0

Li_s(0) = 0.

source

theorem LeanPolyLog.Dilog.hasSum_Li {s : ℕ} (hs : 2 ≤ s) {z : ℂ} (hz : ‖z‖ ≤ 1) :

HasSum (fun (n : ℕ) => z ^ (n + 1) / (↑n + 1) ^ s) (Li s z)

For s ≥ 2 the series of Li_s(z) converges for ‖z‖ ≤ 1.

source

theorem LeanPolyLog.Dilog.continuousOn_Li {s : ℕ} (hs : 2 ≤ s) :

ContinuousOn (Li s) (Metric.closedBall 0 1)

For s ≥ 2, Li_s is continuous on the closed unit disk.

source

theorem LeanPolyLog.Dilog.Li_one {z : ℂ} (hz : ‖z‖ < 1) :

Li 1 z = -Complex.log (1 - z)

Li_1(z) = -log(1 - z) on the open unit disk.

source

theorem LeanPolyLog.Dilog.hasDerivAt_Li_succ (s : ℕ) {z : ℂ} (hz : ‖z‖ < 1) (hz0 : z ≠ 0) :

HasDerivAt (Li (s + 1)) (Li s z / z) z

d/dz Li_(s+1)(z) = Li_s(z)/z for 0 < ‖z‖ < 1.

source

theorem LeanPolyLog.Dilog.hasDerivAt_Li_two {z : ℂ} (hz : ‖z‖ < 1) (hz0 : z ≠ 0) :

HasDerivAt (Li 2) (-Complex.log (1 - z) / z) z

d/dz Li_2(z) = -log(1 - z)/z for 0 < ‖z‖ < 1.

source

theorem LeanPolyLog.Dilog.ofReal_Lir (s : ℕ) (x : ℝ) :

↑(Lir s x) = Li s ↑x

On real arguments Li_s agrees with the real series Lir s.

source

theorem LeanPolyLog.Dilog.Li_sq {s : ℕ} (hs : 2 ≤ s) {z : ℂ} (hz : ‖z‖ ≤ 1) :

Li s (z ^ 2) = 2 ^ (s - 1) * (Li s z + Li s (-z))

The duplication formula Li_s(z²) = 2^(s-1) (Li_s(z) + Li_s(-z)) for ‖z‖ ≤ 1, s ≥ 2.

Constancy from a vanishing derivative #

source

theorem LeanPolyLog.Dilog.eq_of_hasDerivAt_eq_zero_complex {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hc : ContinuousOn f (Set.Icc a b)) (hd : ∀ x ∈ Set.Ioo a b, HasDerivAt f 0 x) :

f a = f b

A complex function of a real variable that is continuous on [a, b] and has derivative 0 on (a, b) takes the same value at a and b.

Landen's identity #

source

theorem LeanPolyLog.Dilog.norm_le_norm_sub_one {a : ℂ} (h : 2 * a.re ≤ 1) :

‖a‖ ≤ ‖a - 1‖

If 2 Re a ≤ 1, then a is at least as close to 0 as to 1.

source

theorem LeanPolyLog.Dilog.norm_lt_norm_sub_one {a : ℂ} (h : 2 * a.re < 1) :

‖a‖ < ‖a - 1‖

If 2 Re a < 1, then a is closer to 0 than to 1.

source

theorem LeanPolyLog.Dilog.Li_two_add_Li_two_div_sub_one {z : ℂ} (hz : ‖z‖ ≤ 1) (hre : z.re ≤ 1 / 2) :

Li 2 z + Li 2 (z / (z - 1)) = -(Complex.log (1 - z) ^ 2 / 2)

Landen's identity Li_2(z) + Li_2(z/(z-1)) = -½ log²(1 - z), for ‖z‖ ≤ 1 and Re z ≤ 1/2 (so that also ‖z/(z-1)‖ ≤ 1).

Proof: along the segment t ↦ t z, t ∈ [0, 1], the function Li_2(tz) + Li_2(tz/(tz-1)) + ½ log²(1 - tz) has derivative 0 and vanishes at t = 0.