Theory Polylog.Polylog
section ‹The Polylogarithm Function›
theory Polylog
imports
"HOL-Complex_Analysis.Complex_Analysis"
"Linear_Recurrences.Eulerian_Polynomials"
"HOL-Real_Asymp.Real_Asymp"
Polylog_Library
begin
subsection ‹Definition and basic properties›
text ‹
The principal branch of the Polylogarithm function $\text{Li}_s(z)$ is defined as
\[\text{Li}_s(z) = \sum_{k=1}^\infty \frac{z^k}{k^s}\]
for $|z|<1$ and elsewhere by analytic continuation. For integer $s \leq 0$ it is holomorphic
except for a pole at $z = 1$. For other values of $s$ it is holomorphic except for a branch
cut along the line $[1, \infty)$.
Special values include $\text{Li}_0(z) = \frac{z}{1-z}$ and $\text{Li}_1(z) = -\log (1-z)$.
One could potentially generalise this to arbitrary ‹s ∈ ℂ›, but this makes the analytic
continuation somewhat more complicated, so we chosed not to do this at this point.
In the following, we define the principal branch of $\text{Li}_s(z)$ for integer $s$.
›
definition polylog :: "int ⇒ complex ⇒ complex" where
"polylog k z =
(if k ≤ 0 then z * poly (eulerian_poly (nat (-k))) z * (1 - z) powi (k - 1)
else if z ∈ of_real ` {1..} then 0
else (SOME f. f holomorphic_on -of_real`{1..} ∧
(∀z∈ball 0 1. f z = (∑n. of_nat (Suc n) powi (-k) * z ^ Suc n))) z)"
lemma conv_radius_polylog: "conv_radius (λr. of_nat r powi k :: complex) = 1"
proof (rule conv_radius_ratio_limit_ereal_nonzero)
have "(λn. ereal (real n powi k / real (Suc n) powi k)) ⇢ ereal 1"
proof (cases "k ≥ 0")
case True
have "(λn. ereal (real n ^ nat k / real (Suc n) ^ nat k)) ⇢ ereal 1"
by (intro tendsto_ereal) real_asymp
thus ?thesis
using True by (simp add: power_int_def)
next
case False
have "(λn. ereal (inverse (real n) ^ nat (-k) / inverse (real (Suc n)) ^ nat (-k))) ⇢ ereal 1"
by (intro tendsto_ereal) real_asymp
thus ?thesis
using False by (simp add: power_int_def)
qed
thus "(λn. ereal (norm (of_nat n powi k :: complex) / norm (of_nat (Suc n) powi k :: complex))) ⇢ 1"
unfolding one_ereal_def [symmetric] by (simp add: norm_power_int del: of_nat_Suc)
qed auto
lemma abs_summable_polylog:
"norm z < 1 ⟹ summable (λr. norm (of_nat r powi k * z ^ r :: complex))"
by (rule abs_summable_in_conv_radius) (use conv_radius_polylog[of k] in auto)
text ‹
Two very central results that characterise the polylogarithm:
\[\text{Li}_s'(z) = \frac{1}{z}\text{Li}_{s-1}(z)\quad\quad\text{and}\quad\quad
\text{Li}_s(z) = \sum_{n=1}^\infty \frac{z^n}{n^s}\quad\text{for}\ |z|<1\]
›
theorem has_field_derivative_polylog [derivative_intros]:
"⋀z. z ∈ (if k ≤ 0 then -{1} else -(of_real ` {1..})) ⟹
(polylog k has_field_derivative (if z = 0 then 1 else polylog (k - 1) z / z)) (at z within A)"
and sums_polylog: "norm z < 1 ⟹ (λn. of_nat (Suc n) powi (-k) * z ^ Suc n) sums polylog k z"
proof -
let ?S = "-(complex_of_real ` {1..})"
have "open ?S"
by (intro open_Compl closed_slot_right)
define S where "S = (λk::int. if k ≤ 0 then -{1} else ?S)"
have [simp]: "open (S k)" for k
using ‹open ?S› by (auto simp: S_def)
have *: "(∀z∈S k. (polylog k has_field_derivative (if z = 0 then 1 else polylog (k - 1) z / z)) (at z)) ∧
(∀z∈ball 0 1. (λn. of_nat (Suc n) powi (-k) * z ^ Suc n) sums polylog k z)"
proof (induction "nat k" arbitrary: k)
case 0
define k' where "k' = nat (-k)"
have k_eq: "k = -int k'"
using 0 by (simp add: k'_def)
have "(polylog k has_field_derivative (if z = 0 then 1 else polylog (k - 1) z / z)) (at z)"
if z: "z ∈ S k" for z
proof -
have [simp]: "z ≠ 1"
using z 0 by (auto simp: S_def)
write eulerian_poly ("E")
have "polylog (k - 1) z = z * (poly (E (Suc k')) z * (1 - z) powi (k - 2))"
using 0 by (simp add: polylog_def k_eq nat_add_distrib algebra_simps)
also have "… = z * poly (E (Suc k')) z / (1 - z) ^ (k' + 2)"
by (simp add: k_eq power_int_def nat_add_distrib field_simps)
finally have eq1: "polylog (k - 1) z = …" .
have "polylog k = (λz. z * poly (E k') z * (1 - z) powi (k - 1))"
using 0 by (simp add: polylog_def [abs_def] k_eq)
also have "… = (λz. z * poly (E k') z / (1 - z) ^ Suc k')"
by (simp add: k_eq power_int_def field_simps nat_add_distrib)
finally have eq2: "polylog k = (λz. z * poly (E k') z / (1 - z) ^ Suc k')" .
have "((λz. z * poly (E k') z / (1 - z) ^ Suc k') has_field_derivative
(poly (E (Suc k')) z / (1 - z) ^ (k' + 2))) (at z)"
apply (rule derivative_eq_intros refl poly_DERIV)+
apply (simp)
apply (simp add: eulerian_poly.simps(2) Let_def divide_simps)
apply (simp add: algebra_simps)
done
also note eq2 [symmetric]
also have "poly (E (Suc k')) z / (1 - z) ^ (k' + 2) =
(if z = 0 then 1 else polylog (k - 1) z / z)"
by (subst eq1) (auto)
finally show ?thesis .
qed
moreover have "(λn. of_nat (Suc n) powi (-k) * z ^ Suc n) sums polylog k z"
if z: "norm z < 1" for z
proof (cases "k = 0")
case True
thus ?thesis using z geometric_sums[of z]
by (auto simp: polylog_def divide_inverse intro!: sums_mult)
next
case False
with 0 have k: "k < 0"
by simp
define F where "F = Abs_fps (λn. of_nat n ^ nat (-k) :: complex)"
have "fps_conv_radius (1 - fps_X :: complex fps) ≥ ∞"
by (intro order.trans[OF _ fps_conv_radius_diff]) auto
hence [simp]: "fps_conv_radius (1 - fps_X :: complex fps) = ∞"
by simp
have *: "fps_conv_radius ((1 - fps_X) ^ (nat (-k) + 1) :: complex fps) ≥ ∞"
by (intro order.trans[OF _ fps_conv_radius_power]) auto
have "ereal (norm z) < 1"
using that by simp
also have "1 ≤ fps_conv_radius F"
unfolding F_def fps_conv_radius_def using conv_radius_polylog[of "-k"] 0
by (simp add: power_int_def)
finally have "(λn. fps_nth F n * z ^ n) sums eval_fps F z"
by (rule sums_eval_fps)
also have "(λn. fps_nth F n * z ^ n) = (λn. of_nat n powi (-k) * z ^ n)"
using 0 by (simp add: F_def power_int_def)
also have "eval_fps F z = poly (fps_monom_poly 1 (nat (- k))) z /
eval_fps ((1 - fps_X) ^ (nat (- k) + 1)) z"
unfolding F_def fps_monom_aux
proof (subst eval_fps_divide')
show "fps_conv_radius (fps_of_poly (fps_monom_poly 1 (nat (- k)))) > 0"
by simp
show "fps_conv_radius ((1 - fps_X :: complex fps) ^ (nat (- k) + 1)) > 0"
by (intro less_le_trans[OF _ fps_conv_radius_power]) auto
show "1 > (0 :: ereal)"
by simp
show "eval_fps ((1 - fps_X) ^ (nat (-k) + 1)) z ≠ 0"
if "z ∈ eball 0 1" for z :: complex
using that by (subst eval_fps_power) (auto simp: eval_fps_diff)
show "ereal (norm z) < Min {1, fps_conv_radius (fps_of_poly (fps_monom_poly 1 (nat (- k)))),
fps_conv_radius ((1 - fps_X :: complex fps) ^ (nat (- k) + 1))}" using * z
by auto
qed auto
also have "eval_fps ((1 - fps_X) ^ (nat (- k) + 1)) z = (1 - z) ^ (nat (-k) + 1)"
by (subst eval_fps_power) (auto simp: eval_fps_diff)
also have "… = (1 - z) powi int (nat (-k) + 1)"
by (rule power_int_of_nat [symmetric])
also have "int (nat (-k) + 1) = -(k-1)"
using 0 by simp
also have "(poly (fps_monom_poly 1 (nat (- k))) z / (1 - z) powi - (k - 1)) = polylog k z"
using k
by (auto simp add: fps_monom_poly_def polylog_def power_int_diff)
finally show "(λn. of_nat (Suc n) powi - k * z ^ (Suc n)) sums polylog k z"
by (subst sums_Suc_iff) (use k in auto)
qed
ultimately show ?case
using 0 by (auto simp: polylog_def [abs_def])
next
case (Suc k' k)
have [simp]: "nat k = Suc k'" "nat (k - 1) = k'"
using Suc(2) by auto
from Suc(2) have k: "k > 0"
by linarith
have deriv: "(polylog (k - 1) has_field_derivative
(if z = 0 then 1 else polylog (k - 2) z / z)) (at z)" if "z ∈ S (k - 1)" for z
using Suc(1)[of "k-1"] that by auto
hence holo: "polylog (k - 1) holomorphic_on S (k - 1)"
by (subst holomorphic_on_open) auto
have sums: "(λn. of_nat (Suc n) powi -(k-1) * z ^ Suc n) sums polylog (k-1) z"
if "norm z < 1" for z
using that Suc(1)[of "k - 1"] by auto
define g where "g = (λz. if z = 0 then 1 else polylog (k - 1) z / z)"
have "g holomorphic_on S (k - 1)"
unfolding g_def
proof (rule removable_singularity)
show "(λz. polylog (k - 1) z / z) holomorphic_on S (k - 1) - {0}"
using Suc by (intro holomorphic_intros holomorphic_on_subset[OF holo]) auto
define F where "F = Abs_fps (λn. of_nat (Suc n) powi (1-k) :: complex)"
have radius: "fls_conv_radius (fps_to_fls F) = 1"
proof -
have "F = fps_shift 1 (Abs_fps (λn. of_int n powi (1 - k)))"
using k by (simp add: F_def fps_eq_iff power_int_def)
also have "fps_conv_radius … = 1"
using conv_radius_polylog[of "1 - k"] unfolding fps_conv_radius_shift
by (simp add: fps_conv_radius_def)
finally show ?thesis by simp
qed
have "eventually (λz::complex. z ∈ ball 0 1) (nhds 0)"
by (intro eventually_nhds_in_open) auto
hence "eventually (λz::complex. z ∈ ball 0 1 - {0}) (at 0)"
unfolding eventually_at_filter by eventually_elim auto
hence "eventually (λz. eval_fls (fps_to_fls F) z = polylog (k - 1) z / z) (at 0)"
proof eventually_elim
case (elim z)
have "(λn. of_nat (Suc n) powi - (k - 1) * z ^ Suc n / z) sums (polylog (k - 1) z / z)"
by (intro sums_divide sums) (use elim in auto)
also have "(λn. of_nat (Suc n) powi - (k - 1) * z ^ Suc n / z) =
(λn. of_nat (Suc n) powi - (k - 1) * z ^ n)"
using elim by auto
finally have "polylog (k - 1) z / z = (∑n. of_nat (Suc n) powi - (k - 1) * z ^ n)"
by (simp add: sums_iff)
also have "… = eval_fps F z"
unfolding eval_fps_def F_def by simp
finally show ?case
using radius elim by (simp add: eval_fps_to_fls)
qed
hence "(λz. polylog (k - 1) z / z) has_laurent_expansion fps_to_fls F"
unfolding has_laurent_expansion_def using radius by auto
hence "(λz. polylog (k - 1) z / z) ─0→ fls_nth (fps_to_fls F) 0"
by (intro has_laurent_expansion_imp_tendsto_0 fls_subdegree_fls_to_fps_gt0) auto
thus "(λy. polylog (k - 1) y / y) ─0→ 1"
by (simp add: F_def)
qed auto
hence holo: "g holomorphic_on ?S"
by (rule holomorphic_on_subset) (auto simp: S_def)
have "simply_connected ?S"
by (rule simply_connected_slotted_complex_plane_right)
then obtain f where f: "⋀z. z ∈ ?S ⟹ (f has_field_derivative g z) (at z)"
using simply_connected_eq_global_primitive holo ‹open ?S› by blast
define h where "h = (λz. f z - f 0)"
have deriv_h [derivative_intros]: "(h has_field_derivative g z) (at z)" if "z ∈ ?S" for z
unfolding h_def using that by (auto intro!: derivative_eq_intros f)
hence holo_h: "h holomorphic_on S k" (is "?P1 h")
by (subst holomorphic_on_open) (use k ‹open ?S› in ‹auto simp: S_def›)
have summable: "summable (λn. of_nat n powi (-k) * z ^ n)"
if "norm z < 1" for z :: complex
by (rule summable_in_conv_radius)
(use that conv_radius_polylog[of "-k"] in auto)
define F where "F = Abs_fps (λn. of_nat n powi (-k) :: complex)"
have radius: "fps_conv_radius F = 1"
using conv_radius_polylog[of "-k"] by (simp add: fps_conv_radius_def F_def)
have F_deriv [derivative_intros]:
"(eval_fps F has_field_derivative g z) (at z)" if "z ∈ ball 0 1" for z
proof -
have "(eval_fps F has_field_derivative eval_fps (fps_deriv F) z) (at z)"
using that radius by (auto intro!: derivative_eq_intros)
also have "eval_fps (fps_deriv F) z = g z"
proof (cases "z = 0")
case False
have "(λn. of_nat (Suc n) powi - (k - 1) * z ^ Suc n / z) sums (polylog (k - 1) z / z)"
by (intro sums_divide sums) (use that in auto)
also have "… = g z"
using False by (simp add: g_def)
also have "(λn. of_nat (Suc n) powi - (k - 1) * z ^ Suc n / z) =
(λn. of_nat (Suc n) powi - (k - 1) * z ^ n)"
using False by simp
finally show ?thesis
by (auto simp add: eval_fps_def F_def sums_iff power_int_diff power_int_minus field_simps
simp del: of_nat_Suc)
qed (auto simp: F_def g_def eval_fps_at_0)
finally show ?thesis .
qed
hence h_eq_sum: "h z = eval_fps F z" if "z ∈ ball 0 1" for z
proof -
have "∃c. ∀z∈ball 0 1. h z - eval_fps F z = c"
proof (rule has_field_derivative_zero_constant)
fix z :: complex assume z: "z ∈ ball 0 1"
have "((λx. h x - eval_fps F x) has_field_derivative 0) (at z)"
using z by (auto intro!: derivative_eq_intros)
thus "((λx. h x - eval_fps F x) has_field_derivative 0) (at z within ball 0 1)"
using z by (subst at_within_open) auto
qed auto
then obtain c where c: "⋀z. norm z < 1 ⟹ h z - eval_fps F z = c"
by force
from c[of 0] and k have "c = 0"
by (simp add: h_def F_def eval_fps_at_0)
thus ?thesis
using c[of z] that by auto
qed
have h_eq_sum': "(∀z∈ball 0 1. h z = (∑n. of_nat (Suc n) powi - k * z ^ Suc n))" (is "?P2 h")
proof safe
fix z :: complex assume z: "z ∈ ball 0 1"
have "summable (λn. of_nat (Suc n) powi - k * z ^ Suc n)"
using z summable[of z] by (subst summable_Suc_iff) auto
also have "?this ⟷ summable (λn. of_nat n powi - k * z ^ n)"
by (rule summable_Suc_iff)
finally have "(λn. of_nat (Suc n) powi -k * z ^ Suc n) sums h z"
using h_eq_sum[of z] k unfolding summable_Suc_iff
by (subst sums_Suc_iff) (use z in ‹auto simp: eval_fps_def F_def›)
thus "h z = (∑n. of_nat (Suc n) powi - k * z ^ Suc n)"
by (simp add: sums_iff)
qed
define h' where "h' = (SOME h. ?P1 h ∧ ?P2 h)"
have "∃h. ?P1 h ∧ ?P2 h"
using h_eq_sum' holo_h by blast
from someI_ex[OF this] have h'_props: "?P1 h'" "?P2 h'"
unfolding h'_def by blast+
have h'_eq: "h' z = polylog k z" if "z ∈ S k" for z
using that k by (auto simp: polylog_def h'_def S_def)
have polylog_sums: "(λn. of_nat (Suc n) powi (-k) * z ^ Suc n) sums polylog k z"
if "norm z < 1" for z
proof -
have "summable (λn. of_nat (Suc n) powi (-k) * z ^ Suc n)"
using summable[of z] that by (subst summable_Suc_iff)
moreover from that have "z ∈ S k"
by (auto simp: S_def)
ultimately show ?thesis
using h'_props using that by (force simp: sums_iff h'_eq)
qed
have eq': "polylog k z = h z" if "z ∈ S k" for z
proof -
have "h' z = h z"
proof (rule analytic_continuation_open[where g = h])
show "h' holomorphic_on S k" "h holomorphic_on S k"
by fact+
show "ball 0 1 ≠ ({} :: complex set)" "open (ball 0 1 :: complex set)"
by auto
show "open (S k)" "connected (S k)" "ball 0 1 ⊆ S k"
using k ‹open ?S› simply_connected_slotted_complex_plane_right[of 1]
by (auto simp: S_def simply_connected_imp_connected)
show "z ∈ S k"
by fact
show "h' z = h z" if "z ∈ ball 0 1" for z
using h'_props(2) h_eq_sum' that by simp
qed
with that show ?thesis
by (simp add: h'_eq)
qed
have deriv_polylog: "(polylog k has_field_derivative g z) (at z)" if "z ∈ S k" for z
proof -
have "(h has_field_derivative g z) (at z)"
by (intro deriv_h) (use that k in ‹auto simp: S_def›)
also have "?this ⟷ ?thesis"
proof (rule DERIV_cong_ev)
have "eventually (λw. w ∈ S k) (nhds z)"
by (intro eventually_nhds_in_open) (use that in auto)
thus "eventually (λw. h w = polylog k w) (nhds z)"
by eventually_elim (auto simp: eq')
qed auto
finally show ?thesis .
qed
show ?case
using deriv_polylog polylog_sums unfolding g_def by simp
qed
show "(polylog k has_field_derivative (if z = 0 then 1 else polylog (k - 1) z / z)) (at z within A)"
if "z ∈ (if k ≤ 0 then -{1} else -(of_real ` {1..}))" for z
using * that unfolding S_def by (blast intro: has_field_derivative_at_within)
show "(λn. of_nat (Suc n) powi (-k) * z ^ Suc n) sums polylog k z" if "norm z < 1" for z
using * that by force
qed
lemma has_field_derivative_polylog' [derivative_intros]:
assumes "(f has_field_derivative f') (at z within A)"
assumes "if k ≤ 0 then f z ≠ 1 else Im (f z) ≠ 0 ∨ Re (f z) < 1"
shows "((λz. polylog k (f z)) has_field_derivative
(if f z = 0 then 1 else polylog (k-1) (f z) / f z) * f') (at z within A)"
proof -
have "(polylog k ∘ f has_field_derivative
(if f z = 0 then 1 else polylog (k-1) (f z) / f z) * f') (at z within A)"
using assms(2) by (intro DERIV_chain assms has_field_derivative_polylog) auto
thus ?thesis
by (simp add: o_def)
qed
lemma polylog_0 [simp]: "polylog k 0 = 0"
proof -
have "(λ_. 0) sums polylog k 0"
using sums_polylog[of 0 k] by simp
moreover have "(λ_. 0 :: complex) sums 0"
by simp
ultimately show ?thesis
using sums_unique2 by blast
qed
text ‹
A simple consequence of the derivative formula is the following recurrence for $\text{Li}_s$
via a contour integral:
\[\text{Li}_s(z) = \int_0^z \frac{1}{w}\text{Li}_{s-1}(w)\,\text{d}w\]
›
theorem polylog_has_contour_integral:
assumes "z ∉ complex_of_real ` ({..-1} ∪ {1..})"
shows "((λw. polylog s w / w) has_contour_integral polylog (s + 1) z) (linepath 0 z)"
proof -
let ?l = "linepath 0 z"
define A where "A = -complex_of_real ` ({..-1} ∪ {1..})"
have "((λw. if w = 0 then 1 else polylog s w / w) has_contour_integral
(polylog (s + 1) (pathfinish ?l) - polylog (s + 1) (pathstart ?l))) (linepath 0 z)"
proof (rule contour_integral_primitive)
have [simp]: "complex_of_real x = -1 ⟷ x = -1" for x
by (simp add: Complex_eq_neg_1 complex_of_real_def)
show "(polylog (s + 1) has_field_derivative (if z = 0 then 1 else polylog s z / z))
(at z within A)" if "z ∈ A" for z
using that by (intro derivative_eq_intros) (auto simp: A_def split: if_splits)
next
show "valid_path (linepath 0 z)"
by (rule valid_path_linepath)
next
show "path_image (linepath 0 z) ⊆ A"
using assms starlike_doubly_slotted_complex_plane_aux[of z "-1" 1 0]
by (auto simp: A_def)
qed
hence "((λw. if w = 0 then 1 else polylog s w / w) has_contour_integral
(polylog (s + 1) z)) (linepath 0 z)"
by simp
thus ?thesis
unfolding has_contour_integral_def
proof (rule has_integral_spike[rotated 2])
show "negligible {0 :: real}"
by simp
qed (auto simp: vector_derivative_linepath_within)
qed
lemma sums_polylog':
"norm z < 1 ⟹ k ≠ 0 ⟹ (λn. of_nat n powi - k * z ^ n) sums polylog k z"
using sums_polylog[of z k] by (subst (asm) sums_Suc_iff) auto
lemma polylog_altdef1:
"norm z < 1 ⟹ polylog k z = (∑n. of_nat (Suc n) powi -k * z ^ Suc n)"
using sums_polylog[of z k] by (simp add: sums_iff)
lemma polylog_altdef2:
"norm z < 1 ⟹ k ≠ 0 ⟹ polylog k z = (∑n. of_nat n powi -k * z ^ n)"
using sums_polylog'[of z k] by (simp add: sums_iff)
lemma polylog_at_pole: "polylog k 1 = 0"
by (auto simp: polylog_def)
lemma polylog_at_branch_cut: "x ≥ 1 ⟹ k > 0 ⟹ polylog k (of_real x) = 0"
by (auto simp: polylog_def)
lemma holomorphic_on_polylog [holomorphic_intros]:
assumes "A ⊆ (if k ≤ 0 then -{1} else -of_real ` {1..})"
shows "polylog k holomorphic_on A"
proof -
let ?S = "-(complex_of_real ` {1..})"
have *: "open ?S"
by (intro open_Compl closed_slot_right)
have "polylog k holomorphic_on (if k ≤ 0 then -{1} else ?S)"
by (subst holomorphic_on_open) (use * in ‹auto intro!: derivative_eq_intros exI›)
thus ?thesis
by (rule holomorphic_on_subset) (use assms in ‹auto split: if_splits›)
qed
lemmas holomorphic_on_polylog' [holomorphic_intros] =
holomorphic_on_compose_gen [OF _ holomorphic_on_polylog[OF order.refl], unfolded o_def]
lemma analytic_on_polylog [analytic_intros]:
assumes "A ⊆ (if k ≤ 0 then -{1} else -of_real ` {1..})"
shows "polylog k analytic_on A"
proof -
let ?S = "-(complex_of_real ` {1..})"
have *: "open ?S"
by (intro open_Compl closed_slot_right)
have "polylog k analytic_on (if k ≤ 0 then -{1} else ?S)"
by (subst analytic_on_open) (use * in ‹auto intro!: holomorphic_intros›)
thus ?thesis
by (rule analytic_on_subset) (use assms in ‹auto split: if_splits›)
qed
lemmas analytic_on_polylog' [analytic_intros] =
analytic_on_compose_gen [OF _ analytic_on_polylog[OF order.refl], unfolded o_def]
lemma continuous_on_polylog [analytic_intros]:
assumes "A ⊆ (if k ≤ 0 then -{1} else -of_real ` {1..})"
shows "continuous_on A (polylog k)"
proof -
let ?S = "-(complex_of_real ` {1..})"
have *: "open ?S"
by (intro open_Compl closed_slot_right)
have "continuous_on (if k ≤ 0 then -{1} else ?S) (polylog k)"
by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto
thus ?thesis
by (rule continuous_on_subset) (use assms in auto)
qed
lemmas continuous_on_polylog' [continuous_intros] =
continuous_on_compose2 [OF continuous_on_polylog [OF order.refl]]
subsection ‹Special values›
lemma polylog_neg_int_left:
"k < 0 ⟹ polylog k z = z * poly (eulerian_poly (nat (-k))) z * (1 - z) powi (k - 1)"
by (auto simp: polylog_def)
lemma polylog_0_left: "polylog 0 z = z / (1 - z)"
by (simp add: polylog_def field_simps)
lemma polylog_neg1_left: "polylog (-1) x = x / (1 - x) ^ 2"
by (simp add: polylog_neg_int_left eval_nat_numeral eulerian_poly.simps
power_int_minus field_simps)
lemma polylog_neg2_left: "polylog (-2) x = x * (1 + x) / (1 - x) ^ 3"
by (simp add: polylog_neg_int_left eval_nat_numeral eulerian_poly.simps
power_int_minus field_simps)
lemma polylog_neg3_left: "polylog (-3) x = x * (1 + 4 * x + x⇧2) / (1 - x) ^ 4"
by (simp add: polylog_neg_int_left eval_nat_numeral eulerian_poly.simps Let_def pderiv_add
pderiv_pCons power_int_minus field_simps numeral_poly)
lemma polylog_1:
assumes "z ∉ of_real ` {1..}"
shows "polylog 1 z = -ln (1 - z)"
proof -
have "(λz. polylog 1 z + ln (1 - z)) constant_on -of_real ` {1..}"
proof (rule has_field_derivative_0_imp_constant_on)
show "connected (-complex_of_real ` {1..})"
using starlike_slotted_complex_plane_right[of 1] starlike_imp_connected by blast
show "open (- complex_of_real ` {1..})"
using closed_slot_right by blast
show "((λz. polylog 1 z + ln (1 - z)) has_field_derivative 0) (at z)"
if "z ∈ -of_real ` {1..}" for z
using that
by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff
complex_slot_right_eq polylog_0_left divide_simps)
qed
then obtain c where c: "⋀z. z ∈ -of_real`{1..} ⟹ polylog 1 z + ln (1 - z) = c"
unfolding constant_on_def by blast
from c[of 0] have "c = 0"
by (auto simp: complex_slot_right_eq)
with c[of z] show ?thesis
using assms by (auto simp: add_eq_0_iff)
qed
lemma is_pole_polylog_1:
assumes "k ≤ 0"
shows "is_pole (polylog k) 1"
proof (cases "k = 0")
case True
have "filtermap (λz. -z) (filtermap (λz. z - 1) (at 1)) = filtermap (λz. -z) (at (0 :: complex))"
by (simp add: at_to_0' filtermap_filtermap)
also have "… = at 0"
by (subst filtermap_at_minus) auto
finally have "filtermap ((λz. -z) ∘ (λz. z - 1)) (at 1) = at (0 :: complex)"
unfolding filtermap_compose .
hence *: "filtermap (λz. 1 - z) (at 1) = at (0 :: complex)"
by (simp add: o_def)
have "is_pole (λz::complex. z / (1 - z)) 1"
unfolding is_pole_def
by (rule filterlim_divide_at_infinity tendsto_intros)+
(use * in ‹auto simp: filterlim_def›)
also have "(λz. z / (1 - z)) = polylog k"
using True by (auto simp: fun_eq_iff polylog_0_left)
finally show ?thesis .
next
case False
have "∀⇩F x in at 1. x ≠ (1 :: complex)"
using eventually_at zero_less_one by blast
hence ev: "∀⇩F x in at 1. 1 - x ≠ (0 :: complex)"
by eventually_elim auto
have "is_pole (λz::complex. z * poly (eulerian_poly (nat (- k))) z * (1 - z) powi (k - 1)) 1"
unfolding is_pole_def
by (rule tendsto_mult_filterlim_at_infinity tendsto_eq_intros refl ev
filterlim_power_int_neg_at_infinity | (use assms in simp; fail))+
also have "(λz::complex. z * poly (eulerian_poly (nat (- k))) z * (1 - z) powi (k - 1)) =
polylog k"
using assms False by (intro ext) (simp add: polylog_neg_int_left)
finally show ?thesis .
qed
lemma zorder_polylog_1:
assumes "k ≤ 0"
shows "zorder (polylog k) 1 = k - 1"
proof (cases "k = 0")
case True
have "filtermap (λz. -z) (filtermap (λz. z - 1) (at 1)) = filtermap (λz. -z) (at (0 :: complex))"
by (simp add: at_to_0' filtermap_filtermap)
also have "… = at 0"
by (subst filtermap_at_minus) auto
finally have "filtermap ((λz. -z) ∘ (λz. z - 1)) (at 1) = at (0 :: complex)"
unfolding filtermap_compose .
hence *: "filtermap (λz. 1 - z) (at 1) = at (0 :: complex)"
by (simp add: o_def)
have "zorder (λz::complex. (-z) / (z - 1) ^ 1) 1 = -int 1"
by (rule zorder_nonzero_div_power [of UNIV]) (auto intro!: holomorphic_intros)
also have "(λz. (-z) / (z - 1) ^ 1) = polylog k"
using True by (auto simp: fun_eq_iff polylog_0_left divide_simps) (auto simp: algebra_simps)?
finally show ?thesis
using True by simp
next
case False
have "zorder (λz::complex. (-1) ^ nat (1 - k) * z * poly (eulerian_poly (nat (- k))) z /
(z - 1) ^ nat (1 - k)) 1 = -int (nat (1 - k))" (is "zorder ?f _ = _")
using False assms
by (intro zorder_nonzero_div_power [of UNIV]) (auto intro!: holomorphic_intros)
also have "?f = polylog k"
proof
fix z :: complex
have "(z - 1) ^ nat (1 - k) = (-1) ^ nat (1 - k) * (1 - z) ^ nat (1 - k)"
by (subst power_mult_distrib [symmetric]) auto
thus "?f z = polylog k z"
using False assms by (auto simp: polylog_neg_int_left power_int_def field_simps)
qed
finally show ?thesis
using False assms by simp
qed
lemma isolated_singularity_polylog_1:
assumes "k ≤ 0"
shows "isolated_singularity_at (polylog k) 1"
unfolding isolated_singularity_at_def using assms
by (intro exI[of _ 1]) (auto intro!: analytic_intros)
lemma not_essential_polylog_1:
assumes "k ≤ 0"
shows "not_essential (polylog k) 1"
unfolding not_essential_def using is_pole_polylog_1[of k] assms by auto
lemma polylog_meromorphic_on [meromorphic_intros]:
assumes "k ≤ 0"
shows "polylog k meromorphic_on {1}"
using assms
by (simp add: isolated_singularity_polylog_1 meromorphic_at_iff not_essential_polylog_1)
subsection ‹Duplication formula›
text ‹
Lastly, we prove the following duplication formula that the polylogarithm satisfies:
\[\text{Li}_s(z) + \text{Li}_s(-z) = 2^{1-s} \text{Li}_s(z^2)\]
The proof is a relatively simple manipulation of infinite sum that defines $\text{Li}_s(z)$
for $|z|<1$, followed by analytic continuation to its full domain.
›
theorem polylog_duplication:
assumes "if s ≤ 0 then z ∉ {-1, 1} else z ∉ complex_of_real ` ({..-1} ∪ {1..})"
shows "polylog s z + polylog s (-z) = 2 powi (1 - s) * polylog s (z⇧2)"
proof -
define A where "A = -(if s ≤ 0 then {-1, 1} else complex_of_real ` ({..-1} ∪ {1..}))"
show ?thesis
proof (rule analytic_continuation_open[where f = "λz. polylog s z + polylog s (-z)"])
show "ball 0 1 ⊆ A"
by (auto simp: A_def)
next
have "closed (complex_of_real ` ({..-1} ∪ {1..}))"
unfolding image_Un by (intro open_Compl closed_Un closed_slot_right closed_slot_left)
thus "open A"
unfolding A_def by auto
next
have "connected (-complex_of_real ` ({..-1} ∪ {1..}))"
by (intro simply_connected_imp_connected simply_connected_doubly_slotted_complex_plane) auto
moreover have "connected (-{-1, 1 :: complex})"
by (intro path_connected_imp_connected path_connected_complement_countable) auto
ultimately show "connected A"
unfolding A_def by auto
next
show "(λz. polylog s z + polylog s (- z)) holomorphic_on A"
by (intro holomorphic_intros) (auto simp: complex_eq_iff A_def)
next
show "(λz. 2 powi (1 - s) * polylog s (z⇧2)) holomorphic_on A"
proof (intro holomorphic_intros; safe)
fix z assume z: "z ∈ A"
show "z^2 ∈ (if s ≤ 0 then - {1} else - complex_of_real ` {1..})"
proof (cases "s ≤ 0")
case True
thus ?thesis using z by (auto simp: A_def power2_eq_1_iff)
next
case False
{
fix x :: real
assume x: "x ≥ 1" "z ^ 2 = of_real x"
have "Im (z ^ 2) = 0"
by (simp add: x)
hence "Im z = 0 ∨ Re z = 0"
by (simp add: power2_eq_square)
moreover have "Im z ^ 2 ≥ 0"
by auto
hence "Im z ^ 2 > -1"
by linarith
ultimately have "x = Re z ^ 2" "Im z = 0"
using x unfolding power2_eq_square by (auto simp: complex_eq_iff)
with x have "¦Re z¦ ≥ 1"
by (auto simp: power2_ge_1_iff)
with ‹Im z = 0› have "z ∉ A"
using False by (auto simp: A_def complex_double_slot_eq)
}
with False show ?thesis using z
by (auto simp: A_def)
qed
qed
next
show "polylog s z + polylog s (-z) = 2 powi (1 - s) * polylog s (z⇧2)"
if z: "z ∈ ball 0 1" for z
proof -
have ran: "range (λn::nat. Suc (2 * n)) = {n. odd n}"
by (auto simp: image_def elim!: oddE)
have "(λn. of_nat (Suc n) powi -s * (z ^ Suc n + (-z) ^ Suc n)) sums
(polylog s z + polylog s (-z))" (is "?f sums _")
unfolding ring_distribs using z
by (intro sums_add sums_mult sums_polylog) (simp_all add: norm_power)
also have "?this ⟷ (λn. ?f (2 * n + 1)) sums (polylog s z + polylog s (-z))"
by (rule sym, intro sums_mono_reindex) (auto simp: ran strict_mono_def)
also have "(λn. ?f (2 * n + 1)) = (λn. 2 * (2 * of_nat (Suc n)) powi -s * (z⇧2) ^ Suc n)"
by (intro ext) (simp_all add: algebra_simps power_mult power2_eq_square power_minus')
also have "… = (λn. 2 powi (1 - s) * (of_nat (Suc n) powi -s * (z⇧2) ^ Suc n))" (is "_ = ?g")
by (simp add: power_int_diff power_int_minus fun_eq_iff field_simps
flip: power_int_mult_distrib)
finally have "?g sums (polylog s z + polylog s (-z))" .
moreover have "?g sums (2 powi (1 - s) * polylog s (z⇧2))"
using z by (intro sums_mult sums_polylog) (simp_all add: norm_power abs_square_less_1)
ultimately show ?thesis
using sums_unique2 by blast
qed
qed (use assms in ‹auto simp: A_def›)
qed
end