Special values for the trilogarithm integrals of A014

Values of Li₂, Li₃ and log at the points ±i and (1 ± i)/2 of the closed unit disk, and a few elementary facts shared by LeanPool.PolylogIntegrals.Lemmas.TrilogLogOneAddSq and LeanPool.PolylogIntegrals.Lemmas.TrilogLogSubLogSq.

Main results

• LeanPolyLog.Trilog.Li_conj: Li_s(conj z) = conj (Li_s(z)).
• LeanPolyLog.Trilog.im_Li_three_I, LeanPolyLog.Trilog.im_Li_three_neg_I: Im Li₃(±i) = ±β(3) = ±π³/32.
• LeanPolyLog.Trilog.im_Li_three_one_sub_I_div_two: Im Li₃((1-i)/2) = -Im Li₃((1+i)/2).
• LeanPolyLog.Trilog.im_Li_two_I, LeanPolyLog.Trilog.im_Li_two_one_sub_I_div_two: Im Li₂(i) = G and Im Li₂((1-i)/2) = (π/8) log 2 - G (from A001 and A002).
• LeanPolyLog.Trilog.log_one_sub_I_div_two, LeanPolyLog.Trilog.log_one_add_I_div_two: log((1 ∓ i)/2) = -½ log 2 ∓ (π/4) i.
• LeanPolyLog.Trilog.im_ofReal_div_sub_I: Im (a/(x - i)) = a/(1 + x²) for real a, x; this is how 1/(1 + x²) arises as an imaginary part.

Proof sketch

• Conjugation commutes with the series, since conj is continuous and additive.
• Im Li₃(i) = ∑ Im(iⁿ⁺¹)/(n+1)³: the terms with n odd vanish and those with n = 2k are (-1)ᵏ/(2k+1)³, which sum to β(3) = π³/32 (LeanPolyLog.Arctan.hasSum_beta_three).
• (1 - i)/2 = (1/2)(1 - i), so its logarithm is -log 2 + log(1 - i), and (1 + i)/2 is its conjugate, whose argument -π/4 is not π.

Conjugation

theorem LeanPolyLog.Trilog.Li_conj (s : ℕ) (z : ℂ) : Li s ((starRingEnd ℂ) z) = (starRingEnd ℂ) (Li s z)

Li_s(conj z) = conj (Li_s(z)).

Values of Li₃ and Li₂

theorem LeanPolyLog.Trilog.im_Li_three_I : (Li 3 Complex.I).im = Real.pi ^ 3 / 32

Im Li₃(i) = β(3) = π³/32.

theorem LeanPolyLog.Trilog.im_Li_three_neg_I : (Li 3 (-Complex.I)).im = -(Real.pi ^ 3 / 32)

Im Li₃(-i) = -π³/32.

theorem LeanPolyLog.Trilog.im_Li_three_one_sub_I_div_two : (Li 3 ((1 - Complex.I) / 2)).im = -(Li 3 ((1 + Complex.I) / 2)).im

Im Li₃((1-i)/2) = -Im Li₃((1+i)/2).

theorem LeanPolyLog.Trilog.one_sub_I_ne_zero : 1 - Complex.I ≠ 0

1 - i ≠ 0.

theorem LeanPolyLog.Trilog.one_sub_I_div_two : (1 - Complex.I) / 2 = 1 / (1 + Complex.I)

(1-i)/2 = 1/(1+i).

theorem LeanPolyLog.Trilog.im_Li_two_one_sub_I_div_two : (Li 2 ((1 - Complex.I) / 2)).im = Real.pi / 8 * Real.log 2 - G

Im Li₂((1-i)/2) = (π/8) log 2 - G (A002).

theorem LeanPolyLog.Trilog.im_Li_two_I : (Li 2 Complex.I).im = G

Im Li₂(i) = G (A001).

Values of log

theorem LeanPolyLog.Trilog.log_one_sub_I_div_two : Complex.log ((1 - Complex.I) / 2) = ↑(-(Real.log 2 / 2)) - ↑(Real.pi / 4) * Complex.I

log((1-i)/2) = -½ log 2 - (π/4) i.

theorem LeanPolyLog.Trilog.log_one_add_I_div_two : Complex.log ((1 + Complex.I) / 2) = ↑(-(Real.log 2 / 2)) + ↑(Real.pi / 4) * Complex.I

log((1+i)/2) = -½ log 2 + (π/4) i.

Elementary facts

theorem LeanPolyLog.Trilog.ofReal_sub_I_ne_zero (x : ℝ) : ↑x - Complex.I ≠ 0

x - i ≠ 0 for real x.

theorem LeanPolyLog.Trilog.im_ofReal_div_sub_I (a x : ℝ) : (↑a / (↑x - Complex.I)).im = a / (1 + x ^ 2)

Im (a/(x - i)) = a/(1 + x²) for real a and x.

theorem LeanPolyLog.Trilog.continuousOn_log_one_add : ContinuousOn (fun (t : ℝ) => Real.log (1 + t)) (Set.Icc 0 1)

x ↦ log(1 + x) is continuous on [0, 1].