Theory Dirichlet_L_Functions
section ‹Dirichlet $L$-functions›
theory Dirichlet_L_Functions
imports
Dirichlet_Characters
"HOL-Library.Landau_Symbols"
"Zeta_Function.Zeta_Function"
begin
text ‹
We can now define the Dirichlet $L$-functions. These are essentially the functions in the complex
plane that the Dirichlet series $\sum_{k=1}^\infty \chi(k) k^{-s}$ converge to, for some fixed
Dirichlet character $\chi$.
First of all, we need to take care of a syntactical problem: The notation for vectors uses
$\chi$ as syntax, which causes some annoyance to us, so we disable it locally.
›
bundle vec_lambda_notation
begin
notation vec_lambda (binder "χ" 10)
end
bundle no_vec_lambda_notation
begin
no_notation vec_lambda (binder "χ" 10)
end
subsection ‹Definition and basic properties›
context
includes no_vec_lambda_notation
begin
text ‹
We now define Dirichlet $L$ functions as a finite linear combination of Hurwitz $\zeta$ functions.
This has the advantage that we directly get the analytic continuation over the full domain
and only need to prove that the series really converges to this definition whenever it
does converge, which is not hard to do.
›
definition Dirichlet_L :: "nat ⇒ (nat ⇒ complex) ⇒ complex ⇒ complex" where
"Dirichlet_L m χ s =
(if s = 1 then
if χ = principal_dchar m then 0 else eval_fds (fds χ) 1
else
of_nat m powr - s * (∑k = 1..m. χ k * hurwitz_zeta (real k / real m) s))"
lemma Dirichlet_L_conv_hurwitz_zeta_nonprincipal:
assumes "s ≠ 1"
shows "Dirichlet_L n χ s =
of_nat n powr -s * (∑k = 1..n. χ k * hurwitz_zeta (real k / real n) s)"
using assms by (simp add: Dirichlet_L_def)
text ‹
Analyticity everywhere except $1$ is trivial by the above definition, since the
Hurwitz $\zeta$ function is analytic everywhere except $1$. For $L$ functions of non
principal characters, we will have to show the analyticity at $1$ separately later.
›
lemma holomorphic_Dirichlet_L_weak:
assumes "m > 0" "1 ∉ A"
shows "Dirichlet_L m χ holomorphic_on A"
proof -
have "(λs. of_nat m powr - s * (∑k = 1..m. χ k * hurwitz_zeta (real k / real m) s))
holomorphic_on A"
using assms unfolding Dirichlet_L_def by (intro holomorphic_intros) auto
also have "?this ⟷ ?thesis"
using assms by (intro holomorphic_cong refl) (auto simp: Dirichlet_L_def)
finally show ?thesis .
qed
end
context dcharacter
begin
context
includes no_vec_lambda_notation dcharacter_syntax
begin
text ‹
For a real value greater than 1, the formal Dirichlet series of an $L$ function
for some character $\chi$ converges to the L function.
›
lemma
fixes s :: complex
assumes s: "Re s > 1"
shows abs_summable_Dirichlet_L: "summable (λn. norm (χ n * of_nat n powr -s))"
and summable_Dirichlet_L: "summable (λn. χ n * of_nat n powr -s)"
and sums_Dirichlet_L: "(λn. χ n * n powr -s) sums Dirichlet_L n χ s"
and Dirichlet_L_conv_eval_fds_weak: "Dirichlet_L n χ s = eval_fds (fds χ) s"
proof -
define L where "L = (∑n. χ n * of_nat n powr -s)"
show "summable (λn. norm (χ n * of_nat n powr -s))"
by (subst summable_Suc_iff [symmetric],
rule summable_comparison_test [OF _ summable_zeta_real[of "Re s"]])
(insert s norm, auto intro!: exI[of _ 0] simp: norm_mult norm_powr_real_powr)
thus summable: "summable (λn. χ n * of_nat n powr -s)"
by (rule summable_norm_cancel)
hence "(λn. χ n * of_nat n powr -s) sums L" by (simp add: L_def sums_iff)
from this have "(λm. ∑k = m * n..<m * n + n. χ k * of_nat k powr - s) sums L"
by (rule sums_group) (use n in auto)
also have "(λm. ∑k = m * n..<m * n + n. χ k * of_nat k powr - s) =
(λm. of_nat n powr -s * (∑k = 1..n. χ k * (of_nat m + of_nat k / of_nat n) powr - s))"
proof (rule ext, goal_cases)
case (1 m)
have "(∑k = m * n..<m * n + n. χ k * of_nat k powr - s) =
(∑k=0..<n. χ (k + m * n) * of_nat (m * n + k) powr - s)"
by (intro sum.reindex_bij_witness[of _ "λk. k + m * n" "λk. k - m * n"]) auto
also have "… = (∑k=0..<n. χ k * of_nat (m * n + k) powr - s)"
by (simp add: periodic_mult)
also have "… = (∑k=0..<n. χ k * (of_nat m + of_nat k / of_nat n) powr - s * of_nat n powr -s)"
proof (intro sum.cong refl, goal_cases)
case (1 k)
have "of_nat (m * n + k) = (of_nat m + of_nat k / of_nat n :: complex) * of_nat n"
using n by (simp add: divide_simps del: div_mult_self1 div_mult_self2 div_mult_self3 div_mult_self4)
also have "… powr -s = (of_nat m + of_nat k / of_nat n) powr -s * of_nat n powr -s"
by (rule powr_times_real) auto
finally show ?case by simp
qed
also have "… = of_nat n powr -s * (∑k=0..<n. χ k * (of_nat m + of_nat k / of_nat n) powr - s)"
by (subst sum_distrib_left) (simp_all add: mult_ac)
also have "(∑k = 0..<n. χ k * (of_nat m + of_nat k / of_nat n) powr - s) =
(∑k = 1..<n. χ k * (of_nat m + of_nat k / of_nat n) powr - s)"
by (intro sum.mono_neutral_right) (auto simp: Suc_le_eq)
also have "… = (∑k = 1..n. χ k * (of_nat m + of_nat k / of_nat n) powr - s)"
using periodic_mult[of 0 1] by (intro sum.mono_neutral_left) auto
finally show ?case .
qed
finally have "… sums L" .
moreover have "(λm. of_nat n powr - s * (∑k=1..n. χ k * (of_nat m + of_real (of_nat k / of_nat n)) powr - s)) sums
(of_nat n powr - s * (∑k=1..n. χ k * hurwitz_zeta (of_nat k / of_nat n) s))"
using s by (intro sums_sum sums_mult sums_hurwitz_zeta) auto
ultimately have "L = …"
by (simp add: sums_iff)
also have "… = Dirichlet_L n χ s" using assms by (auto simp: Dirichlet_L_def)
finally have "Dirichlet_L n χ s = (∑n. χ n * of_nat n powr -s)"
by (simp add: L_def)
with summable show "(λn. χ n * n powr -s) sums Dirichlet_L n χ s"
by (simp add: sums_iff L_def)
thus "Dirichlet_L n χ s = eval_fds (fds χ) s"
by (simp add: eval_fds_def sums_iff powr_minus field_simps fds_nth_fds')
qed
lemma fds_abs_converges_weak: "Re s > 1 ⟹ fds_abs_converges (fds χ) s"
using abs_summable_Dirichlet_L[of s]
by (simp add: fds_abs_converges_def powr_minus divide_simps fds_nth_fds')
lemma abs_conv_abscissa_weak: "abs_conv_abscissa (fds χ) ≤ 1"
proof (rule abs_conv_abscissa_leI, goal_cases)
case (1 c)
thus ?case
by (intro exI[of _ "of_real c"] conjI fds_abs_converges_weak) auto
qed
text ‹
Dirichlet $L$ functions have the Euler product expansion
\[L(\chi, s) = \prod_p \left(1 - \frac{\chi(p)}{p^{-s}}\right)\]
for all $s$ with $\mathfrak{R}(s) > 1$.
›
lemma
fixes s :: complex assumes s: "Re s > 1"
shows Dirichlet_L_euler_product_LIMSEQ:
"(λn. ∏p≤n. if prime p then inverse (1 - χ p / nat_power p s) else 1)
⇢ Dirichlet_L n χ s" (is ?th1)
and Dirichlet_L_abs_convergent_euler_product:
"abs_convergent_prod (λp. if prime p then inverse (1 - χ p / p powr s) else 1)"
(is ?th2)
proof -
have mult: "completely_multiplicative_function (fds_nth (fds χ))"
using mult.completely_multiplicative_function_axioms by (simp add: fds_nth_fds')
have conv: "fds_abs_converges (fds χ) s"
using abs_summable_Dirichlet_L[OF s]
by (simp add: fds_abs_converges_def fds_nth_fds' powr_minus divide_simps)
have "(λn. ∏p≤n. if prime p then inverse (1 - χ p / nat_power p s) else 1)
⇢ eval_fds (fds χ) s"
using fds_euler_product_LIMSEQ' [OF mult conv] by (simp add: fds_nth_fds' cong: if_cong)
also have "eval_fds (fds χ) s = Dirichlet_L n χ s"
using sums_Dirichlet_L[OF s] unfolding eval_fds_def
by (simp add: sums_iff fds_nth_fds' powr_minus divide_simps)
finally show ?th1 .
from fds_abs_convergent_euler_product' [OF mult conv] show ?th2
by (simp add: fds_nth_fds cong: if_cong)
qed
lemma Dirichlet_L_Re_gt_1_nonzero:
assumes "Re s > 1"
shows "Dirichlet_L n χ s ≠ 0"
proof -
have "completely_multiplicative_function (fds_nth (fds χ))"
by (simp add: fds_nth_fds' mult.completely_multiplicative_function_axioms)
moreover have "fds_abs_converges (fds χ) s"
using abs_summable_Dirichlet_L[OF assms]
by (simp add: fds_abs_converges_def fds_nth_fds' powr_minus divide_simps)
ultimately have "(eval_fds (fds χ) s = 0) ⟷ (∃p. prime p ∧ fds_nth (fds χ) p = nat_power p s)"
by (rule fds_abs_convergent_zero_iff)
also have "eval_fds (fds χ) s = Dirichlet_L n χ s"
using Dirichlet_L_conv_eval_fds_weak[OF assms] by simp
also have "¬(∃p. prime p ∧ fds_nth (fds χ) p = nat_power p s)"
proof safe
fix p :: nat assume p: "prime p" "fds_nth (fds χ) p = nat_power p s"
from p have "real 1 < real p" by (subst of_nat_less_iff) (auto simp: prime_gt_Suc_0_nat)
also have "… = real p powr 1" by simp
also from p and assms have "real p powr 1 ≤ real p powr Re s"
by (intro powr_mono) (auto simp: real_of_nat_ge_one_iff prime_ge_Suc_0_nat)
also have "… = norm (nat_power p s)" by (simp add: norm_nat_power norm_powr_real_powr)
also have "nat_power p s = fds_nth (fds χ) p" using p by simp
also have "norm … ≤ 1" by (auto simp: fds_nth_fds' norm)
finally show False by simp
qed
finally show ?thesis .
qed
lemma sum_dcharacter_antimono_bound:
fixes x0 a b :: real and f f' :: "real ⇒ real"
assumes nonprincipal: "χ ≠ χ⇩0"
assumes x0: "x0 ≥ 0" and ab: "x0 ≤ a" "a < b"
assumes f': "⋀x. x ≥ x0 ⟹ (f has_field_derivative f' x) (at x)"
assumes f_nonneg: "⋀x. x ≥ x0 ⟹ f x ≥ 0"
assumes f'_nonpos: "⋀x. x ≥ x0 ⟹ f' x ≤ 0"
shows "norm (∑n∈real -` {a<..b}. χ n * (f (real n))) ≤ 2 * real (totient n) * f a"
proof -
note deriv = has_field_derivative_at_within [OF f']
let ?A = "sum_upto χ"
have cont: "continuous_on {a..b} f"
by (rule DERIV_continuous_on[OF deriv]) (use ab in auto)
have I': "(f' has_integral (f b - f a)) {a..b}"
using ab deriv by (intro fundamental_theorem_of_calculus)
(auto simp: has_real_derivative_iff_has_vector_derivative [symmetric])
define I where "I = integral {a..b} (λt. ?A t * of_real (f' t))"
define C where "C = real (totient n)"
have C_nonneg: "C ≥ 0" by (simp add: C_def)
have C: "norm (?A x) ≤ C" for x
proof -
have "?A x = (∑k≤nat ⌊x⌋. χ k)" unfolding sum_upto_altdef
by (intro sum.mono_neutral_left) auto
also have "norm … ≤ C" unfolding C_def using nonprincipal
by (rule sum_dcharacter_atMost_le)
finally show ?thesis .
qed
have I: "((λt. ?A t * f' t) has_integral ?A b * f b - ?A a * f a -
(∑n∈real -` {a<..b}. χ n * f (real n))) {a..b}" using ab x0 cont f'
by (intro partial_summation_strong[of "{}"] has_vector_derivative_of_real) auto
hence "(∑n∈real -` {a<..b}. χ n * f (real n)) = ?A b * f b - ?A a * f a - I"
by (simp add: has_integral_iff I_def)
also have "norm … ≤ norm (?A b) * norm (f b) + norm (?A a) * norm (f a) + norm I"
by (rule order.trans[OF norm_triangle_ineq4] add_mono)+ (simp_all add: norm_mult)
also have "norm I ≤ integral {a..b} (λt. of_real (-C) * of_real (f' t))"
unfolding I_def using I I' f'_nonpos ab C
by (intro integral_norm_bound_integral integrable_on_cmult_left)
(simp_all add: has_integral_iff norm_mult mult_right_mono_neg)
also have "… = - (C * (f b - f a))"
using integral_linear[OF _ bounded_linear_of_real, of f' "{a..b}"] I'
by (simp add: has_integral_iff o_def )
also have "… = C * (f a - f b)" by (simp add: algebra_simps)
also have "norm (sum_upto χ b) ≤ C" by (rule C)
also have "norm (sum_upto χ a) ≤ C" by (rule C)
also have "C * norm (f b) + C * norm (f a) + C * (f a - f b) = 2 * C * f a"
using f_nonneg[of a] f_nonneg[of b] ab by (simp add: algebra_simps)
finally show ?thesis by (simp add: mult_right_mono C_def)
qed
lemma summable_dcharacter_antimono:
fixes x0 a b :: real and f f' :: "real ⇒ real"
assumes nonprincipal: "χ ≠ χ⇩0"
assumes f': "⋀x. x ≥ x0 ⟹ (f has_field_derivative f' x) (at x)"
assumes f_nonneg: "⋀x. x ≥ x0 ⟹ f x ≥ 0"
assumes f'_nonpos: "⋀x. x ≥ x0 ⟹ f' x ≤ 0"
assumes lim: "(f ⤏ 0) at_top"
shows "summable (λn. χ n * f n)"
proof (rule summable_bounded_partials [where ?g = "λx. 2 * real (totient n) * f x"], goal_cases)
case 1
from eventually_ge_at_top[of "nat ⌈x0⌉"] show ?case
proof eventually_elim
case (elim x)
show ?case
proof (safe, goal_cases)
case (1 a b)
with elim have *: "max 0 x0 ≥ 0" "max 0 x0 ≤ a" "real a < real b"
by (simp_all add: nat_le_iff ceiling_le_iff)
have "(∑n∈{a<..b}. χ n * complex_of_real (f (real n))) =
(∑n∈real -` {real a<..real b}. χ n * complex_of_real (f (real n)))"
by (intro sum.cong refl) auto
also have "norm … ≤ 2 * real (totient n) * f a"
using nonprincipal * f' f_nonneg f'_nonpos by (rule sum_dcharacter_antimono_bound) simp_all
finally show ?case .
qed
qed
qed (auto intro!: tendsto_mult_right_zero filterlim_compose[OF lim] filterlim_real_sequentially)
lemma conv_abscissa_le_0:
fixes s :: real
assumes nonprincipal: "χ ≠ χ⇩0"
shows "conv_abscissa (fds χ) ≤ 0"
proof (rule conv_abscissa_leI)
fix s assume s: "0 < ereal s"
have "summable (λn. χ n * of_real (n powr -s))"
proof (rule summable_dcharacter_antimono[of 1])
fix x :: real assume "x ≥ 1"
thus "((λx. x powr -s) has_field_derivative (-s * x powr (-s-1))) (at x)"
by (auto intro!: derivative_eq_intros)
qed (insert s assms, auto intro!: tendsto_neg_powr filterlim_ident)
thus "∃s'::complex. s' ∙ 1 = s ∧ fds_converges (fds χ) s'" using s
by (intro exI[of _ "of_real s"])
(auto simp: fds_converges_def powr_minus divide_simps powr_of_real [symmetric] fds_nth_fds')
qed
lemma summable_Dirichlet_L':
assumes nonprincipal: "χ ≠ χ⇩0"
assumes s: "Re s > 0"
shows "summable (λn. χ n * of_nat n powr -s)"
proof -
from assms have "fds_converges (fds χ) s"
by (intro fds_converges le_less_trans[OF conv_abscissa_le_0]) auto
thus ?thesis by (simp add: fds_converges_def powr_minus divide_simps fds_nth_fds')
qed
lemma
assumes "χ ≠ χ⇩0"
shows Dirichlet_L_conv_eval_fds: "⋀s. Re s > 0 ⟹ Dirichlet_L n χ s = eval_fds (fds χ) s"
and holomorphic_Dirichlet_L: "Dirichlet_L n χ holomorphic_on A"
proof -
show eq: "Dirichlet_L n χ s = eval_fds (fds χ) s" (is "?f s = ?g s") if "Re s > 0" for s
proof (cases "s = 1")
case False
show ?thesis
proof (rule analytic_continuation_open[where ?f = ?f and ?g = ?g])
show "{s. Re s > 1} ⊆ {s. Re s > 0} - {1}" by auto
show "connected ({s. 0 < Re s} - {1})"
using aff_dim_halfspace_gt[of 0 "1::complex"]
by (intro connected_punctured_convex convex_halfspace_Re_gt) auto
qed (insert that n assms False,
auto intro!: convex_halfspace_Re_gt open_halfspace_Re_gt exI[of _ 2]
holomorphic_intros holomorphic_Dirichlet_L_weak
Dirichlet_L_conv_eval_fds_weak le_less_trans[OF conv_abscissa_le_0])
qed (insert assms, simp_all add: Dirichlet_L_def)
have "Dirichlet_L n χ holomorphic_on UNIV"
proof (rule no_isolated_singularity')
from n show "Dirichlet_L n χ holomorphic_on (UNIV - {1})"
by (intro holomorphic_Dirichlet_L_weak) auto
next
fix s :: complex assume s: "s ∈ {1}"
show "Dirichlet_L n χ ─s→ Dirichlet_L n χ s"
proof (rule Lim_transform_eventually)
from assms have "continuous_on {s. Re s > 0} (eval_fds (fds χ))"
by (intro holomorphic_fds_eval holomorphic_on_imp_continuous_on)
(auto intro: le_less_trans[OF conv_abscissa_le_0])
hence "eval_fds (fds χ) ─s→ eval_fds (fds χ) s" using s
by (subst (asm) continuous_on_eq_continuous_at) (auto simp: open_halfspace_Re_gt isCont_def)
also have "eval_fds (fds χ) s = Dirichlet_L n χ s"
using assms s by (simp add: Dirichlet_L_def)
finally show "eval_fds (fds χ) ─s→ Dirichlet_L n χ s" .
next
have "eventually (λz. z ∈ {z. Re z > 0}) (nhds s)" using s
by (intro eventually_nhds_in_open) (auto simp: open_halfspace_Re_gt)
hence "eventually (λz. z ∈ {z. Re z > 0}) (at s)"
unfolding eventually_at_filter by eventually_elim auto
then show "eventually (λz. eval_fds (fds χ) z = Dirichlet_L n χ z) (at s)"
by eventually_elim (auto intro!: eq [symmetric])
qed
qed auto
thus "Dirichlet_L n χ holomorphic_on A" by (rule holomorphic_on_subset) auto
qed
lemma cnj_Dirichlet_L:
"cnj (Dirichlet_L n χ s) = Dirichlet_L n (inv_character χ) (cnj s)"
proof -
{
assume *: "χ ≠ χ⇩0" "s = 1"
with summable_Dirichlet_L'[of 1] have "(λn. χ n / n) sums eval_fds (fds χ) 1"
by (simp add: eval_fds_def fds_nth_fds' powr_minus sums_iff divide_simps)
hence "(λn. inv_character χ n / n) sums cnj (eval_fds (fds χ) 1)"
by (subst (asm) sums_cnj [symmetric]) (simp add: inv_character_def)
hence "eval_fds (fds (inv_character χ)) 1 = cnj (eval_fds (fds χ) 1)"
by (simp add: eval_fds_def fds_nth_fds' inv_character_def sums_iff)
}
thus ?thesis by (auto simp add: Dirichlet_L_def cnj_powr eval_inv_character)
qed
end
end
context
includes no_vec_lambda_notation
begin
lemma holomorphic_Dirichlet_L [holomorphic_intros]:
assumes "n > 1" "χ ≠ principal_dchar n ∧ dcharacter n χ ∨ χ = principal_dchar n ∧ 1 ∉ A"
shows "Dirichlet_L n χ holomorphic_on A"
using assms(2)
proof
assume "χ = principal_dchar n ∧ 1 ∉ A"
with holomorphic_Dirichlet_L_weak[of n A "principal_dchar n"] assms(1) show ?thesis by auto
qed (insert dcharacter.holomorphic_Dirichlet_L[of n χ A], auto)
lemma holomorphic_Dirichlet_L' [holomorphic_intros]:
assumes "n > 1" "f holomorphic_on A"
"χ ≠ principal_dchar n ∧ dcharacter n χ ∨ χ = principal_dchar n ∧ (∀x∈A. f x ≠ 1)"
shows "(λs. Dirichlet_L n χ (f s)) holomorphic_on A"
using holomorphic_on_compose[OF assms(2) holomorphic_Dirichlet_L[OF assms(1), of χ]] assms
by (auto simp: o_def image_iff)
lemma continuous_on_Dirichlet_L:
assumes "n > 1" "χ ≠ principal_dchar n ∧ dcharacter n χ ∨ χ = principal_dchar n ∧ 1 ∉ A"
shows "continuous_on A (Dirichlet_L n χ)"
using assms by (intro holomorphic_on_imp_continuous_on holomorphic_intros)
lemma continuous_on_Dirichlet_L' [continuous_intros]:
assumes "continuous_on A f" "n > 1"
and "χ ≠ principal_dchar n ∧ dcharacter n χ ∨ χ = principal_dchar n ∧ (∀x∈A. f x ≠ 1)"
shows "continuous_on A (λx. Dirichlet_L n χ (f x))"
using continuous_on_compose2[OF continuous_on_Dirichlet_L[of n χ "f ` A"] assms(1)] assms
by (auto simp: image_iff)
corollary continuous_Dirichlet_L [continuous_intros]:
"n > 1 ⟹ χ ≠ principal_dchar n ∧ dcharacter n χ ∨ χ = principal_dchar n ∧ s ≠ 1 ⟹
continuous (at s within A) (Dirichlet_L n χ)"
by (rule continuous_within_subset[of _ UNIV])
(insert continuous_on_Dirichlet_L[of n χ "(if χ = principal_dchar n then -{1} else UNIV)"],
auto simp: continuous_on_eq_continuous_at open_Compl)
corollary continuous_Dirichlet_L' [continuous_intros]:
"n > 1 ⟹ continuous (at s within A) f ⟹
χ ≠ principal_dchar n ∧ dcharacter n χ ∨ χ = principal_dchar n ∧ f s ≠ 1 ⟹
continuous (at s within A) (λx. Dirichlet_L n χ (f x))"
by (rule continuous_within_compose3[OF continuous_Dirichlet_L]) auto
end
context residues_nat
begin
context
includes no_vec_lambda_notation dcharacter_syntax
begin
text ‹
Applying the above to the $L(\chi_0,s)$, the $L$ function of the principal character, we find
that it differs from the Riemann $\zeta$ function only by multiplication with a constant that
depends only on the modulus $n$. They therefore have the same analytic properties as the $\zeta$
function itself.
›
lemma Dirichlet_L_principal:
fixes s :: complex
shows "Dirichlet_L n χ⇩0 s = (∏p | prime p ∧ p dvd n. (1 - 1 / p powr s)) * zeta s"
(is "?f s = ?g s")
proof (cases "s = 1")
case False
show ?thesis
proof (rule analytic_continuation_open[where ?f = ?f and ?g = ?g])
show "{s. Re s > 1} ⊆ - {1}" by auto
show "?f s = ?g s" if "s ∈ {s. Re s > 1}" for s
proof -
from that have s: "Re s > 1" by simp
let ?P = "(∏p | prime p ∧ p dvd n. (1 - 1 / p powr s))"
have "(λn. ∏p≤n. if prime p then inverse (1 - χ⇩0 p / nat_power p s) else 1)
⇢ Dirichlet_L n χ⇩0 s"
using s by (rule principal.Dirichlet_L_euler_product_LIMSEQ)
also have "?this ⟷ (λn. ?P * (∏p≤n. if prime p then inverse (1 - 1 / of_nat p powr s) else 1))
⇢ Dirichlet_L n χ⇩0 s" (is "_ = filterlim ?g _ _")
proof (intro tendsto_cong eventually_mono [OF eventually_ge_at_top, of n], goal_cases)
case (1 m)
let ?f = "λp. inverse (1 - 1 / p powr s)"
have "(∏p≤m. if prime p then inverse (1 - χ⇩0 p / nat_power p s) else 1) =
(∏p | p ≤ m ∧ prime p ∧ coprime p n. ?f p)" (is "_ = prod _ ?A")
by (intro prod.mono_neutral_cong_right) (auto simp: principal_dchar_def)
also have "?A = {p. p ≤ m ∧ prime p} - {p. prime p ∧ p dvd n}"
(is "_ = ?B - ?C") using n by (auto dest: prime_imp_coprime simp: coprime_absorb_left)
also {
have *: "(∏p∈?B. ?f p) = (∏p∈?B - ?C. ?f p) * (∏p∈?C. ?f p)"
using 1 n by (intro prod.subset_diff) (auto dest: dvd_imp_le)
have "(∏p∈?B. ?f p) * ?P = (∏p∈?B - ?C. ?f p) * ((∏p∈?C. ?f p) * ?P)"
by (subst *) (simp add: mult_ac)
also have "(∏p∈?C. ?f p) * ?P = (∏p∈?C. 1)"
by (subst prod.distrib [symmetric], rule prod.cong)
(insert s, auto simp: divide_simps powr_def exp_eq_1)
also have "… = 1" by simp
finally have "(∏p∈?B - ?C. ?f p) = (∏p∈?B. ?f p) * ?P" by simp
}
also have "(∏p∈?B. ?f p) = (∏p≤m. if prime p then ?f p else 1)"
by (intro prod.mono_neutral_cong_left) auto
finally show ?case by (simp only: mult_ac)
qed
finally have "?g ⇢ Dirichlet_L n χ⇩0 s" .
moreover have "?g ⇢ ?P * zeta s"
by (intro tendsto_mult tendsto_const euler_product_zeta s)
ultimately show "Dirichlet_L n χ⇩0 s = ?P * zeta s"
by (rule LIMSEQ_unique)
qed
qed (insert ‹s ≠ 1› n, auto intro!: holomorphic_intros holomorphic_Dirichlet_L_weak
open_halfspace_Re_gt exI[of _ 2] connected_punctured_universe)
qed (simp_all add: Dirichlet_L_def zeta_1)
end
end
subsection ‹The non-vanishing for $\mathfrak{R}(s)\geq 1$›
lemma coprime_prime_exists:
assumes "n > (0 :: nat)"
obtains p where "prime p" "coprime p n"
proof -
from bigger_prime[of n] obtain p where p: "prime p" "p > n" by auto
with assms have "¬p dvd n" by (auto dest: dvd_imp_le)
with p have "coprime p n" by (intro prime_imp_coprime)
with that[of p] and p show ?thesis by auto
qed
text ‹
The case of the principal character is trivial, since it differs from the Riemann $\zeta(s)$
only in a multiplicative factor that is clearly non-zero for $\mathfrak{R}(s) \geq 1$.
›
theorem (in residues_nat) Dirichlet_L_Re_ge_1_nonzero_principal:
assumes "Re s ≥ 1" "s ≠ 1"
shows "Dirichlet_L n (principal_dchar n) s ≠ 0"
proof -
have "(∏p | prime p ∧ p dvd n. 1 - 1 / p powr s) ≠ (0 :: complex)"
proof (subst prod_zero_iff)
from n show "finite {p. prime p ∧ p dvd n}" by (intro finite_prime_divisors) auto
show "¬(∃p∈{p. prime p ∧ p dvd n}. 1 - 1 / p powr s = 0)"
proof safe
fix p assume p: "prime p" "p dvd n" and "1 - 1 / p powr s = 0"
hence "norm (p powr s) = 1" by simp
also have "norm (p powr s) = real p powr Re s" by (simp add: norm_powr_real_powr)
finally show False using p assms by (simp add: powr_def prime_gt_0_nat)
qed
qed
with zeta_Re_ge_1_nonzero[OF assms] show ?thesis by (simp add: Dirichlet_L_principal)
qed
text ‹
The proof for non-principal character is quite involved and is typically very complicated
and technical in most textbooks. For instance, Apostol~\<^cite>‹"apostol1976analytic"› proves the
result separately for real and non-real characters, where the non-real case is relatively short
and nice, but the real case involves a number of complicated asymptotic estimates.
The following proof, on the other hand -- like our proof of the analogous result for the
Riemann $\zeta$ function -- is based on Newman's book~\<^cite>‹"newman1998analytic"›. Newman gives
a very short, concise, and high-level sketch that we aim to reproduce faithfully here.
›
context dcharacter
begin
context
includes no_vec_lambda_notation dcharacter_syntax
begin
theorem Dirichlet_L_Re_ge_1_nonzero_nonprincipal:
assumes "χ ≠ χ⇩0" and "Re u ≥ 1"
shows "Dirichlet_L n χ u ≠ 0"
proof (cases "Re u > 1")
include dcharacter_syntax
case False
define a where "a = -Im u"
from False and assms have "Re u = 1" by simp
hence [simp]: "u = 1 - 𝗂 * a" by (simp add: a_def complex_eq_iff)
show ?thesis
proof
assume "Dirichlet_L n χ u = 0"
hence zero: "Dirichlet_L n χ (1 - 𝗂 * a) = 0" by simp
define χ' where [simp]: "χ' = inv_character χ"
define Z where "Z = (λs. ∏χ∈dcharacters n. Dirichlet_L n χ s)"
define Z_fds where "Z_fds = (∏χ∈dcharacters n. fds χ)"
define Q where "Q = (λs. Z s ^ 2 * Z (s + 𝗂 * a) * Z (s - 𝗂 * a))"
define Q_fds where "Q_fds = Z_fds ^ 2 * fds_shift (𝗂 * a) Z_fds * fds_shift (-𝗂 * a) Z_fds"
let ?sings = "{1, 1 + 𝗂 * a, 1 - 𝗂 * a}"
define P where "P = (λs. (∏x∈{p. prime p ∧ p dvd n}. 1 - 1 / of_nat x powr s :: complex))"
have χ⇩0: "χ⇩0 ∈ dcharacters n" by (auto simp: principal.dcharacter_axioms dcharacters_def)
have [continuous_intros]: "continuous_on A P" for A unfolding P_def
by (intro continuous_intros) (auto simp: prime_gt_0_nat)
from this[of UNIV] have [continuous_intros]: "isCont P s" for s
by (auto simp: continuous_on_eq_continuous_at)
have χ: "χ ∈ dcharacters n" "χ' ∈ dcharacters n" using dcharacter_axioms
by (auto simp add: dcharacters_def dcharacter.dcharacter_inv_character)
from zero dcharacter.cnj_Dirichlet_L[of n χ "1 - 𝗂 * a"] dcharacter_axioms
have zero': "Dirichlet_L n χ' (1 + 𝗂 * a) = 0" by simp
have "Z = (λs. Dirichlet_L n χ⇩0 s * (∏χ∈dcharacters n - {χ⇩0}. Dirichlet_L n χ s))"
unfolding Z_def using χ⇩0 by (intro ext prod.remove) auto
also have "… = (λs. P s * zeta s * (∏χ∈dcharacters n - {χ⇩0}. Dirichlet_L n χ s))"
by (simp add: Dirichlet_L_principal P_def)
finally have Z_eq: "Z = (λs. P s * zeta s * (∏χ∈dcharacters n - {χ⇩0}. Dirichlet_L n χ s))" .
have Z_eq': "Z = (λs. P s * zeta s * Dirichlet_L n χ s *
(∏χ∈dcharacters n - {χ⇩0} - {χ}. Dirichlet_L n χ s))"
if "χ ∈ dcharacters n" "χ ≠ χ⇩0" for χ
proof (rule ext, goal_cases)
case (1 s)
from that have χ: "χ ∈ dcharacters n" by (simp add: dcharacters_def)
have "Z s = P s * zeta s *
(∏χ∈dcharacters n - {χ⇩0}. Dirichlet_L n χ s)" by (simp add: Z_eq)
also have "(∏χ∈dcharacters n - {χ⇩0}. Dirichlet_L n χ s) = Dirichlet_L n χ s *
(∏χ∈dcharacters n - {χ⇩0} - {χ}. Dirichlet_L n χ s)"
using assms χ that by (intro prod.remove) auto
finally show ?case by (simp add: mult_ac)
qed
have Q_bigo_1: "Q ∈ O[at s](λ_. 1)" for s
proof (cases "a = 0")
case True
have "(λs. Dirichlet_L n χ s - Dirichlet_L n χ 1) ∈ O[at 1](λs. s - 1)" using χ assms n
by (intro taylor_bigo_linear holomorphic_on_imp_differentiable_at[of _ UNIV]
holomorphic_intros) (auto simp: dcharacters_def)
hence *: "Dirichlet_L n χ ∈ O[at 1](λs. s - 1)" using zero True by simp
have "Z = (λs. P s * zeta s * Dirichlet_L n χ s *
(∏χ∈dcharacters n - {χ⇩0} - {χ}. Dirichlet_L n χ s))"
using χ assms by (intro Z_eq') auto
also have "… ∈ O[at 1](λs. 1 * (1 / (s - 1)) * (s - 1) * 1)" using n χ
by (intro landau_o.big.mult continuous_imp_bigo_1 zeta_bigo_at_1 continuous_intros *)
(auto simp: dcharacters_def)
also have "(λs::complex. 1 * (1 / (s - 1)) * (s - 1) * 1) ∈ Θ[at 1](λ_. 1)"
by (intro bigthetaI_cong) (auto simp: eventually_at_filter)
finally have Z_at_1: "Z ∈ O[at 1](λ_. 1)" .
have "Z ∈ O[at s](λ_. 1)"
proof (cases "s = 1")
case False
thus ?thesis unfolding Z_def using n χ
by (intro continuous_imp_bigo_1 continuous_intros) (auto simp: dcharacters_def)
qed (insert Z_at_1, auto)
from ‹a = 0› have "Q = (λs. Z s * Z s * Z s * Z s)"
by (simp add: Q_def power2_eq_square)
also have "… ∈ O[at s](λ_. 1 * 1 * 1 * 1)"
by (intro landau_o.big.mult) fact+
finally show ?thesis by simp
next
case False
have bigo1: "(λs. Z s * Z (s - 𝗂 * a)) ∈ O[at 1](λ_. 1)"
if "Dirichlet_L n χ (1 - 𝗂 * a) = 0" "a ≠ 0" "χ ∈ dcharacters n" "χ ≠ χ⇩0"
for a :: real and χ
proof -
have "(λs. Dirichlet_L n χ (s - 𝗂 * a) - Dirichlet_L n χ (1 - 𝗂 * a)) ∈ O[at 1](λs. s - 1)"
using assms n that
by (intro taylor_bigo_linear holomorphic_on_imp_differentiable_at[of _ UNIV]
holomorphic_intros) (auto simp: dcharacters_def)
hence *: "(λs. Dirichlet_L n χ (s - 𝗂 * a)) ∈ O[at 1](λs. s - 1)" using that by simp
have "(λs. Z (s - 𝗂*a)) = (λs. P (s - 𝗂*a) * zeta (s - 𝗂*a) * Dirichlet_L n χ (s - 𝗂*a)
* (∏χ∈dcharacters n - {χ⇩0} - {χ}. Dirichlet_L n χ (s - 𝗂*a)))"
using that by (subst Z_eq'[of χ]) auto
also have "… ∈ O[at 1](λs. 1 * 1 * (s - 1) * 1)" unfolding P_def using that n
by (intro landau_o.big.mult continuous_imp_bigo_1 continuous_intros *)
(auto simp: prime_gt_0_nat dcharacters_def)
finally have "(λs. Z (s - 𝗂 * a)) ∈ O[at 1](λs. s - 1)" by simp
moreover have "Z ∈ O[at 1](λs. 1 * (1 / (s - 1)) * 1)" unfolding Z_eq using n that
by (intro landau_o.big.mult zeta_bigo_at_1 continuous_imp_bigo_1 continuous_intros)
(auto simp: dcharacters_def)
hence "Z ∈ O[at 1](λs. 1 / (s - 1))" by simp
ultimately have "(λs. Z s * Z (s - 𝗂 * a)) ∈ O[at 1](λs. 1 / (s - 1) * (s - 1))"
by (intro landau_o.big.mult)
also have "(λs. 1 / (s - 1) * (s - 1)) ∈ Θ[at 1](λ_. 1)"
by (intro bigthetaI_cong) (auto simp add: eventually_at_filter)
finally show ?thesis .
qed
have bigo1': "(λs. Z s * Z (s + 𝗂 * a)) ∈ O[at 1](λ_. 1)"
if "Dirichlet_L n χ (1 - 𝗂 * a) = 0" "a ≠ 0" "χ ∈ dcharacters n" "χ ≠ χ⇩0"
for a :: real and χ
proof -
from that interpret dcharacter n G χ by (simp_all add: dcharacters_def G_def)
from bigo1[of "inv_character χ" "-a"] that cnj_Dirichlet_L[of "1 - 𝗂 * a"] show ?thesis
by (simp add: dcharacters_def dcharacter_inv_character)
qed
have bigo2: "(λs. Z s * Z (s - 𝗂 * a)) ∈ O[at (1 + 𝗂 * a)](λ_. 1)"
if "Dirichlet_L n χ (1 - 𝗂 * a) = 0" "a ≠ 0" "χ ∈ dcharacters n" "χ ≠ χ⇩0"
for a :: real and χ
proof -
have "(λs. Z s * Z (s - 𝗂 * a)) ∈ O[filtermap (λs. s + 𝗂 * a) (at 1)](λ_. 1)"
using bigo1'[of χ a] that by (simp add: mult.commute landau_o.big.in_filtermap_iff)
also have "filtermap (λs. s + 𝗂 * a) (at 1) = at (1 + 𝗂 * a)"
using filtermap_at_shift[of "-𝗂 * a" 1] by simp
finally show ?thesis .
qed
have bigo2': "(λs. Z s * Z (s + 𝗂 * a)) ∈ O[at (1 - 𝗂 * a)](λ_. 1)"
if "Dirichlet_L n χ (1 - 𝗂 * a) = 0" "a ≠ 0" "χ ∈ dcharacters n" "χ ≠ χ⇩0"
for a :: real and χ
proof -
from that interpret dcharacter n G χ by (simp_all add: dcharacters_def G_def)
from bigo2[of "inv_character χ" "-a"] that cnj_Dirichlet_L[of "1 - 𝗂 * a"] show ?thesis
by (simp add: dcharacters_def dcharacter_inv_character)
qed
have Q_eq: "Q = (λs. (Z s * Z (s + 𝗂 * a)) * (Z s * Z (s - 𝗂 * a)))"
by (simp add: Q_def power2_eq_square mult_ac)
consider "s = 1" | "s = 1 + 𝗂 * a" | "s = 1 - 𝗂 * a" | "s ∉ ?sings" by blast
thus ?thesis
proof cases
case 1
have "Q ∈ O[at 1](λ_. 1 * 1)"
unfolding Q_eq using assms zero zero' False χ
by (intro landau_o.big.mult bigo1[of χ a] bigo1'[of χ a]; simp)+
with 1 show ?thesis by simp
next
case 2
have "Q ∈ O[at (1 + 𝗂 * a)](λ_. 1 * 1)" unfolding Q_eq
using assms zero zero' False χ n
by (intro landau_o.big.mult bigo2[of χ a] continuous_imp_bigo_1)
(auto simp: Z_def dcharacters_def intro!: continuous_intros)
with 2 show ?thesis by simp
next
case 3
have "Q ∈ O[at (1 - 𝗂 * a)](λ_. 1 * 1)" unfolding Q_eq
using assms zero zero' False χ n
by (intro landau_o.big.mult bigo2'[of χ a] continuous_imp_bigo_1)
(auto simp: Z_def dcharacters_def intro!: continuous_intros)
with 3 show ?thesis by simp
next
case 4
thus ?thesis unfolding Q_def Z_def using n
by (intro continuous_imp_bigo_1 continuous_intros)
(auto simp: dcharacters_def complex_eq_iff)
qed
qed
have "∃Q'. Q' holomorphic_on UNIV ∧ (∀z∈UNIV - ?sings. Q' z = Q z)"
using n by (intro removable_singularities Q_bigo_1)
(auto simp: Q_def Z_def dcharacters_def complex_eq_iff intro!: holomorphic_intros)
then obtain Q' where Q': "Q' holomorphic_on UNIV" "⋀z. z ∉ ?sings ⟹ Q' z = Q z" by blast
have eval_Q_fds: "eval_fds Q_fds s = Q' s" if "Re s > 1" for s
proof -
have [simp]: "dcharacter n χ" if "χ ∈ dcharacters n" for χ
using that by (simp add: dcharacters_def)
from that have "abs_conv_abscissa (fds χ) < ereal (Re s)" if "χ ∈ dcharacters n" for χ
using that by (intro le_less_trans[OF dcharacter.abs_conv_abscissa_weak[of n χ]]) auto
hence "eval_fds Q_fds s = Q s" using that
by (simp add: Q_fds_def Q_def eval_fds_mult eval_fds_power fds_abs_converges_mult
eval_fds_prod fds_abs_converges_prod dcharacter.Dirichlet_L_conv_eval_fds_weak
fds_abs_converges_power eval_fds_zeta Z_fds_def Z_def fds_abs_converges)
also from that have "… = Q' s" by (subst Q') auto
finally show ?thesis .
qed
define I where "I = (λk. if [k = 1] (mod n) then totient n else 0 :: real)"
have ln_Q_fds_eq:
"fds_ln 0 Q_fds = fds (λk. of_real (2 * I k * mangoldt k / ln k * (1 + cos (a * ln k))))"
proof -
have nz: "χ (Suc 0) = 1" if "χ ∈ dcharacters n" for χ
using dcharacter.Suc_0[of n χ] that by (simp add: dcharacters_def)
note simps = fds_ln_mult[where l' = 0 and l'' = 0] fds_ln_power[where l' = 0]
fds_ln_prod[where l' = "λ_. 0"]
have "fds_ln 0 Q_fds = (∑χ∈dcharacters n. 2 * fds_ln 0 (fds χ) +
fds_shift (𝗂 * a) (fds_ln 0 (fds χ)) + fds_shift (-𝗂 * a) (fds_ln 0 (fds χ)))"
by (auto simp: Q_fds_def Z_fds_def simps nz sum.distrib sum_distrib_left)
also have "… = (∑χ∈dcharacters n.
fds (λk. χ k * of_real (2 * mangoldt k / ln k * (1 + cos (a * ln k)))))"
(is "(∑χ∈_. ?l χ) = _")
proof (intro sum.cong refl, goal_cases)
case (1 χ)
then interpret dcharacter n G χ by (simp_all add: dcharacters_def G_def)
have mult: "completely_multiplicative_function (fds_nth (fds χ))"
by (simp add: fds_nth_fds' mult.completely_multiplicative_function_axioms)
have *: "fds_ln 0 (fds χ) = fds (λn. χ n * mangoldt n /⇩R ln (real n))"
by (simp add: fds_ln_completely_multiplicative[OF mult] fds_nth_fds' fds_eq_iff)
have "?l χ = fds (λk. χ k * mangoldt k /⇩R ln k * (2 + k powr (𝗂 * a) + k powr (-𝗂 * a)))"
by (unfold *, rule fds_eqI) (simp add: algebra_simps scaleR_conv_of_real numeral_fds)
also have "… = fds (λk. χ k * 2 * mangoldt k /⇩R ln k * (1 + cos (of_real(a * ln k))))"
unfolding cos_exp_eq by (intro fds_eqI) (simp add: powr_def algebra_simps)
also have "… = fds (λk. χ k * of_real (2 * mangoldt k / ln k * (1 + cos (a * ln k))))"
unfolding cos_of_real by (simp add: field_simps scaleR_conv_of_real)
finally show ?case .
qed
also have "… = fds (λk. (∑χ∈dcharacters n. χ k) * of_real (2 * mangoldt k / ln k *
(1 + cos (a * ln k))))"
by (simp add: sum_distrib_right sum_divide_distrib scaleR_conv_of_real sum_distrib_left)
also have "… = fds (λk. of_real (2 * I k * mangoldt k / ln k * (1 + cos (a * ln k))))"
by (intro fds_eqI, subst sum_dcharacters) (simp_all add: I_def algebra_simps)
finally show ?thesis .
qed
have "nonneg_dirichlet_series (fds_ln 0 Q_fds)"
proof
show "fds_nth (fds_ln 0 Q_fds) k ∈ ℝ⇩≥⇩0" for k
proof (cases "k < 2")
case False
have cos: "1 + cos x ≥ 0" for x :: real
using cos_ge_minus_one[of x] by linarith
have "fds_nth (fds_ln 0 Q_fds) k =
of_real (2 * I k * mangoldt k / ln k * (1 + cos (a * ln k)))"
by (auto simp: fds_nth_fds' ln_Q_fds_eq)
also have "… ∈ ℝ⇩≥⇩0" using False unfolding I_def
by (subst nonneg_Reals_of_real_iff)
(intro mult_nonneg_nonneg divide_nonneg_pos cos mangoldt_nonneg, auto)
finally show ?thesis .
qed (cases k; auto simp: ln_Q_fds_eq)
qed
hence nonneg: "nonneg_dirichlet_series Q_fds"
proof (rule nonneg_dirichlet_series_lnD)
have "(∏x∈dcharacters n. x (Suc 0)) = 1"
by (intro prod.neutral) (auto simp: dcharacters_def dcharacter.Suc_0)
thus "exp 0 = fds_nth Q_fds (Suc 0)" by (simp add: Q_fds_def Z_fds_def)
qed
have "abs_conv_abscissa Q_fds ≤ 1" unfolding Q_fds_def Z_fds_def fds_shift_prod
by (intro abs_conv_abscissa_power_leI abs_conv_abscissa_mult_leI abs_conv_abscissa_prod_le)
(auto simp: dcharacters_def dcharacter.abs_conv_abscissa_weak)
with nonneg and eval_Q_fds and ‹Q' holomorphic_on UNIV›
have abscissa: "abs_conv_abscissa Q_fds = -∞"
by (intro entire_continuation_imp_abs_conv_abscissa_MInfty[where g = Q' and c = 1])
(auto simp: one_ereal_def)
from n obtain p where p: "prime p" "coprime p n"
using coprime_prime_exists[of n] by auto
define R_fds where "R_fds = fds_primepow_subseries p Q_fds"
have "conv_abscissa R_fds ≤ abs_conv_abscissa R_fds" by (rule conv_le_abs_conv_abscissa)
also have "abs_conv_abscissa R_fds ≤ abs_conv_abscissa Q_fds"
unfolding R_fds_def by (rule abs_conv_abscissa_restrict)
also have "… = -∞" by (simp add: abscissa)
finally have abscissa': "conv_abscissa R_fds = -∞" by simp
define g :: "real ⇒ complex ⇒ complex"
where "g = (λa s. (∏χ∈dcharacters n. (1 - χ p * p powr (-s + 𝗂 * of_real a))))"
have g_nz: "g a s ≠ 0" if "Re s > 0" for s a unfolding g_def
proof (subst prod_zero_iff[OF finite_dcharacters], safe)
fix χ assume "χ ∈ dcharacters n" and *: "1 - χ p * p powr (-s + 𝗂*a) = 0"
then interpret dcharacter n G χ by (simp_all add: dcharacters_def G_def)
from p have "real p > real 1" by (subst of_nat_less_iff) (auto simp: prime_gt_Suc_0_nat)
hence "real p powr - Re s < real p powr 0"
using p that by (intro powr_less_mono) auto
hence "0 < norm (1 :: complex) - norm (χ p * p powr (-s + 𝗂*a))"
using p by (simp add: norm_mult norm norm_powr_real_powr)
also have "… ≤ norm (1 - χ p * p powr (-s + 𝗂*a))"
by (rule norm_triangle_ineq2)
finally show False by (subst (asm) *) simp_all
qed
have [holomorphic_intros]: "g a holomorphic_on A" for a A unfolding g_def
using p by (intro holomorphic_intros)
have eval_R: "eval_fds R_fds s = 1 / (g 0 s ^ 2 * g a s * g (-a) s)"
(is "_ = ?f s") if "Re s > 0" for s :: complex
proof -
show ?thesis
proof (rule analytic_continuation_open[where f = "eval_fds R_fds"])
show "?f holomorphic_on {s. Re s > 0}" using p g_nz[of 0] g_nz[of a] g_nz[of "-a"]
by (intro holomorphic_intros) (auto simp: g_nz)
next
fix z assume z: "z ∈ {s. Re s > 1}"
have [simp]: "completely_multiplicative_function χ" "fds_nth (fds χ) = χ"
if "χ ∈ dcharacters n" for χ
proof -
from that interpret dcharacter n G χ by (simp_all add: G_def dcharacters_def)
show "completely_multiplicative_function χ" "fds_nth (fds χ) = χ"
by (simp_all add: fds_nth_fds' mult.completely_multiplicative_function_axioms)
qed
have [simp]: "dcharacter n χ" if "χ ∈ dcharacters n" for χ
using that by (simp add: dcharacters_def)
from that have "abs_conv_abscissa (fds χ) < ereal (Re z)" if "χ ∈ dcharacters n" for χ
using that z by (intro le_less_trans[OF dcharacter.abs_conv_abscissa_weak[of n χ]]) auto
thus "eval_fds R_fds z = ?f z" using z p
by (simp add: R_fds_def Q_fds_def Z_fds_def eval_fds_mult eval_fds_prod eval_fds_power
fds_abs_converges_mult fds_abs_converges_power fds_abs_converges_prod g_def mult_ac
fds_primepow_subseries_euler_product_cm powr_minus powr_diff powr_add prod_dividef
fds_abs_summable_zeta g_nz fds_abs_converges power_one_over divide_inverse [symmetric])
qed (insert that abscissa', auto intro!: exI[of _ 2] convex_connected open_halfspace_Re_gt
convex_halfspace_Re_gt holomorphic_intros)
qed
show False
proof (rule not_tendsto_and_filterlim_at_infinity)
have g_limit: "(g a ⤏ g a 0) (at 0 within {s. Re s > 0})" for a
proof -
have "continuous_on UNIV (g a)" by (intro holomorphic_on_imp_continuous_on holomorphic_intros)
hence "isCont (g a) 0" by (rule continuous_on_interior) auto
hence "continuous (at 0 within {s. Re s > 0}) (g a)" by (rule continuous_within_subset) auto
thus ?thesis by (auto simp: continuous_within)
qed
have "((λs. g 0 s ^ 2 * g a s * g (-a) s) ⤏ g 0 0 ^ 2 * g a 0 * g (-a) 0)
(at 0 within {s. Re s > 0})" by (intro tendsto_intros g_limit)
also have "g 0 0 = 0" unfolding g_def
proof (rule prod_zero)
from p and χ⇩0 show "∃χ∈dcharacters n. 1 - χ p * of_nat p powr (- 0 + 𝗂 * of_real 0) = 0"
by (intro bexI[of _ χ⇩0]) (auto simp: principal_dchar_def)
qed auto
moreover have "eventually (λs. s ∈ {s. Re s > 0}) (at 0 within {s. Re s > 0})"
by (auto simp: eventually_at_filter)
hence "eventually (λs. g 0 s ^ 2 * g a s * g (-a) s ≠ 0) (at 0 within {s. Re s > 0})"
by eventually_elim (auto simp: g_nz)
ultimately have "filterlim (λs. g 0 s ^ 2 * g a s * g (-a) s) (at 0)
(at 0 within {s. Re s > 0})" by (simp add: filterlim_at)
hence "filterlim ?f at_infinity (at 0 within {s. Re s > 0})" (is ?lim)
by (intro filterlim_divide_at_infinity[OF tendsto_const]
tendsto_mult_filterlim_at_infinity) auto
also have ev: "eventually (λs. Re s > 0) (at 0 within {s. Re s > 0})"
by (auto simp: eventually_at intro!: exI[of _ 1])
have "?lim ⟷ filterlim (eval_fds R_fds) at_infinity (at 0 within {s. Re s > 0})"
by (intro filterlim_cong refl eventually_mono[OF ev]) (auto simp: eval_R)
finally show … .
next
have "continuous (at 0 within {s. Re s > 0}) (eval_fds R_fds)"
by (intro continuous_intros) (auto simp: abscissa')
thus "((eval_fds R_fds ⤏ eval_fds R_fds 0)) (at 0 within {s. Re s > 0})"
by (auto simp: continuous_within)
next
have "0 ∈ {s. Re s ≥ 0}" by simp
also have "{s. Re s ≥ 0} = closure {s. Re s > 0}"
using closure_halfspace_gt[of "1::complex" 0] by (simp add: inner_commute)
finally have "0 ∈ …" .
thus "at 0 within {s. Re s > 0} ≠ bot"
by (subst at_within_eq_bot_iff) auto
qed
qed
qed (fact Dirichlet_L_Re_gt_1_nonzero)
subsection ‹Asymptotic bounds on partial sums of Dirichlet $L$ functions›
text ‹
The following are some bounds on partial sums of the $L$-function of a character that are
useful for asymptotic reasoning, particularly for Dirichlet's Theorem.
›
lemma sum_upto_dcharacter_le:
assumes "χ ≠ χ⇩0"
shows "norm (sum_upto χ x) ≤ totient n"
proof -
have "sum_upto χ x = (∑k≤nat ⌊x⌋. χ k)" unfolding sum_upto_altdef
by (intro sum.mono_neutral_left) auto
also have "norm … ≤ totient n"
by (rule sum_dcharacter_atMost_le) fact
finally show ?thesis .
qed
lemma Dirichlet_L_minus_partial_sum_bound:
fixes s :: complex and x :: real
assumes "χ ≠ χ⇩0" and "Re s > 0" and "x > 0"
defines "σ ≡ Re s"
shows "norm (sum_upto (λn. χ n * n powr -s) x - Dirichlet_L n χ s) ≤
real (totient n) * (2 + cmod s / σ) / x powr σ"
proof (rule Lim_norm_ubound)
from assms have "summable (λn. χ n * of_nat n powr -s)"
by (intro summable_Dirichlet_L')
with assms have "(λn. χ n * of_nat n powr -s) sums Dirichlet_L n χ s"
using Dirichlet_L_conv_eval_fds[OF assms(1,2)]
by (simp add: sums_iff eval_fds_def powr_minus divide_simps fds_nth_fds')
hence "(λm. ∑k≤m. χ k * of_nat k powr -s) ⇢ Dirichlet_L n χ s"
by (simp add: sums_def' atLeast0AtMost)
thus "(λm. sum_upto (λk. χ k * of_nat k powr -s) x - (∑k≤m. χ k * of_nat k powr -s))
⇢ sum_upto (λk. χ k * of_nat k powr -s) x - Dirichlet_L n χ s"
by (intro tendsto_intros)
next
define M where "M = sum_upto χ"
have le: "norm (∑n∈real-`{x<..y}. χ n * of_nat n powr - s)
≤ real (totient n) * (2 + cmod s / σ) / x powr σ" if xy: "0 < x" "x < y" for x y
proof -
from xy have I: "((λt. M t * (-s * t powr (-s-1))) has_integral
M y * of_real y powr - s - M x * of_real x powr - s -
(∑n∈real-`{x<..y}. χ n * of_real (real n) powr -s)) {x..y}" unfolding M_def
by (intro partial_summation_strong [of "{}"])
(auto intro!: has_vector_derivative_real_field derivative_eq_intros continuous_intros)
hence "(∑n∈real-`{x<..y}. χ n * real n powr -s) =
M y * of_real y powr - s - M x * of_real x powr - s -
integral {x..y} (λt. M t * (-s * t powr (-s-1)))"
by (simp add: has_integral_iff)
also have "norm … ≤ norm (M y * of_real y powr -s) + norm (M x * of_real x powr -s) +
norm (integral {x..y} (λt. M t * (-s * t powr (-s-1))))"
by (intro order.trans[OF norm_triangle_ineq4] add_mono order.refl)
also have "norm (M y * of_real y powr -s) ≤ totient n * y powr -σ"
using xy assms unfolding norm_mult M_def σ_def
by (intro mult_mono sum_upto_dcharacter_le) (auto simp: norm_powr_real_powr)
also have "… ≤ totient n * x powr -σ"
using assms xy by (intro mult_left_mono powr_mono2') (auto simp: σ_def)
also have "norm (M x * of_real x powr -s) ≤ totient n * x powr -σ"
using xy assms unfolding norm_mult M_def σ_def
by (intro mult_mono sum_upto_dcharacter_le) (auto simp: norm_powr_real_powr)
also have "norm (integral {x..y} (λt. M t * (- s * of_real t powr (-s-1)))) ≤
integral {x..y} (λt. real (totient n) * norm s * t powr (-σ-1))"
proof (rule integral_norm_bound_integral integrable_on_cmult_left)
show "(λt. real (totient n) * norm s * t powr (- σ - 1)) integrable_on {x..y}"
using xy by (intro integrable_continuous_real continuous_intros) auto
next
fix t assume t: "t ∈ {x..y}"
have "norm (M t * (-s * of_real t powr (-s-1))) ≤
real (totient n) * (norm s * t powr (-σ-1))"
unfolding norm_mult M_def σ_def using xy t assms
by (intro mult_mono sum_upto_dcharacter_le) (auto simp: norm_mult norm_powr_real_powr)
thus "norm (M t * (-s * of_real t powr (-s-1))) ≤ real (totient n) * norm s * t powr (-σ-1)"
by (simp add: algebra_simps)
qed (insert I, auto simp: has_integral_iff)
also have "… = real (totient n) * norm s * integral {x..y} (λt. t powr (-σ-1))"
by simp
also have "((λt. t powr (-σ-1)) has_integral (y powr -σ / (-σ) - x powr -σ / (-σ))) {x..y}"
using xy assms
by (intro fundamental_theorem_of_calculus)
(auto intro!: derivative_eq_intros
simp: has_real_derivative_iff_has_vector_derivative [symmetric] σ_def)
hence "integral {x..y} (λt. t powr (-σ-1)) = y powr -σ / (-σ) - x powr -σ / (-σ)"
by (simp add: has_integral_iff)
also from assms have "… ≤ x powr -σ / σ" by (simp add: σ_def)
also have "real (totient n) * x powr -σ + real (totient n) * x powr -σ +
real (totient n) * norm s * (x powr -σ / σ) =
real (totient n) * (2 + norm s / σ) / x powr σ"
using xy by (simp add: field_simps powr_minus)
finally show ?thesis by (simp add: mult_left_mono)
qed
show "eventually (λm. norm (sum_upto (λk. χ k * of_nat k powr - s) x -
(∑k≤m. χ k * of_nat k powr - s))
≤ real (totient n) * (2 + cmod s / σ) / x powr σ) at_top"
using eventually_gt_at_top[of "nat ⌊x⌋"]
proof eventually_elim
case (elim m)
have "(∑k≤m. χ k * of_nat k powr - s) - sum_upto (λk. χ k * of_nat k powr - s) x =
(∑k∈{..m} - {k. 0 < k ∧ real k ≤ x}. χ k * of_nat k powr -s)" unfolding sum_upto_def
using elim ‹x > 0› by (intro Groups_Big.sum_diff [symmetric])
(auto simp: nat_less_iff floor_less_iff)
also have "… = (∑k∈{..m} - {k. real k ≤ x}. χ k * of_nat k powr -s)"
by (intro sum.mono_neutral_right) auto
also have "{..m} - {k. real k ≤ x} = real -` {x<..real m}"
using elim ‹x > 0› by (auto simp: nat_less_iff floor_less_iff not_less)
also have "norm (∑k∈…. χ k * of_nat k powr -s) ≤
real (totient n) * (2 + cmod s / σ) / x powr σ"
using elim ‹x > 0› by (intro le) (auto simp: nat_less_iff floor_less_iff)
finally show ?case by (simp add: norm_minus_commute)
qed
qed auto
lemma partial_Dirichlet_L_sum_bigo:
fixes s :: complex and x :: real
assumes "χ ≠ χ⇩0" "Re s > 0"
shows "(λx. sum_upto (λn. χ n * n powr -s) x - Dirichlet_L n χ s) ∈ O(λx. x powr -s)"
proof (rule bigoI)
show "eventually (λx. norm (sum_upto (λn. χ n * of_nat n powr -s) x - Dirichlet_L n χ s)
≤ real (totient n) * (2 + norm s / Re s) * norm (of_real x powr - s)) at_top"
using eventually_gt_at_top[of 0]
proof eventually_elim
case (elim x)
have "norm (sum_upto (λn. χ n * of_nat n powr -s) x - Dirichlet_L n χ s)
≤ real (totient n) * (2 + norm s / Re s) / x powr Re s"
using elim assms by (intro Dirichlet_L_minus_partial_sum_bound) auto
thus ?case using elim assms
by (simp add: norm_powr_real_powr powr_minus divide_simps norm_divide
del: div_mult_self1 div_mult_self2 div_mult_self3 div_mult_self4)
qed
qed
end
end
subsection ‹Evaluation of $L(\chi, 0)$›
context residues_nat
begin
context
includes no_vec_lambda_notation dcharacter_syntax
begin
lemma Dirichlet_L_0_principal [simp]: "Dirichlet_L n χ⇩0 0 = 0"
proof -
have "Dirichlet_L n χ⇩0 0 = -1/2 * (∏p | prime p ∧ p dvd n. 1 - 1 / p powr 0)"
by (simp add: Dirichlet_L_principal prime_gt_0_nat)
also have "(∏p | prime p ∧ p dvd n. 1 - 1 / p powr 0) = (∏p | prime p ∧ p dvd n. 0 :: complex)"
by (intro prod.cong) (auto simp: prime_gt_0_nat)
also have "(∏p | prime p ∧ p dvd n. 0 :: complex) = 0"
using prime_divisor_exists[of n] n by (auto simp: card_gt_0_iff)
finally show ?thesis by simp
qed
end
end
context dcharacter
begin
context
includes no_vec_lambda_notation dcharacter_syntax
begin
lemma Dirichlet_L_0_nonprincipal:
assumes nonprincipal: "χ ≠ χ⇩0"
shows "Dirichlet_L n χ 0 = -(∑k=1..<n. of_nat k * χ k) / of_nat n"
proof -
have "Dirichlet_L n χ 0 = (∑k=1..n. χ k * (1 / 2 - of_nat k / of_nat n))"
using assms n by (simp add: Dirichlet_L_conv_hurwitz_zeta_nonprincipal)
also have "… = -1/n * (∑k=1..n. of_nat k * χ k)"
using assms by (simp add: algebra_simps sum_subtractf sum_dcharacter_block'
sum_divide_distrib [symmetric])
also have "(∑k=1..n. of_nat k * χ k) = (∑k=1..<n. of_nat k * χ k)"
using n by (intro sum.mono_neutral_right) (auto simp: eq_zero_iff)
finally show eq: "Dirichlet_L n χ 0 = -(∑k=1..<n. of_nat k * χ k) / of_nat n"
by simp
qed
lemma Dirichlet_L_0_even [simp]:
assumes "χ (n - 1) = 1"
shows "Dirichlet_L n χ 0 = 0"
proof (cases "χ = χ⇩0")
case False
hence "Dirichlet_L n χ 0 = -(∑k=Suc 0..<n. of_nat k * χ k) / of_nat n"
by (simp add: Dirichlet_L_0_nonprincipal)
also have "… = 0"
using assms False by (subst even_dcharacter_linear_sum_eq_0) auto
finally show "Dirichlet_L n χ 0 = 0" .
qed auto
lemma Dirichlet_L_0:
"Dirichlet_L n χ 0 = (if χ (n - 1) = 1 then 0 else -(∑k=1..<n. of_nat k * χ k) / of_nat n)"
by (cases "χ = χ⇩0") (auto simp: Dirichlet_L_0_nonprincipal)
end
end
subsection ‹Properties of $L(\chi, s)$ for real $\chi$›
unbundle no_vec_lambda_notation
locale real_dcharacter = dcharacter +
assumes real: "χ k ∈ ℝ"
begin
lemma Im_eq_0 [simp]: "Im (χ k) = 0"
using real[of k] by (auto elim!: Reals_cases)
lemma of_real_Re [simp]: "of_real (Re (χ k)) = χ k"
by (simp add: complex_eq_iff)
lemma char_cases: "χ k ∈ {-1, 0, 1}"
proof -
from norm[of k] have "Re (χ k) ∈ {-1,0,1}"
by (auto simp: cmod_def split: if_splits)
hence "of_real (Re (χ k)) ∈ {-1, 0, 1}" by auto
also have "of_real (Re (χ k)) = χ k" by (simp add: complex_eq_iff)
finally show ?thesis .
qed
lemma cnj [simp]: "cnj (χ k) = χ k"
by (simp add: complex_eq_iff)
lemma inv_character_id [simp]: "inv_character χ = χ"
by (simp add: inv_character_def fun_eq_iff)
lemma Dirichlet_L_in_Reals:
assumes "s ∈ ℝ"
shows "Dirichlet_L n χ s ∈ ℝ"
proof -
have "cnj (Dirichlet_L n χ s) = Dirichlet_L n χ s"
using assms by (subst cnj_Dirichlet_L) (auto elim!: Reals_cases)
thus ?thesis using Reals_cnj_iff by blast
qed
text ‹
The following property of real characters is used by Apostol to show the non-vanishing of
$L(\chi, 1)$. We have already shown this in a much easier way, but this particular result is
still of general interest.
›
lemma
assumes k: "k > 0"
shows sum_char_divisors_ge: "Re (∑d | d dvd k. χ d) ≥ 0" (is "Re (?A k) ≥ 0")
and sum_char_divisors_square_ge: "is_square k ⟹ Re (∑d | d dvd k. χ d) ≥ 1"
proof -
interpret sum: multiplicative_function ?A
by (fact mult.multiplicative_sum_divisors)
have A: "?A k ∈ ℝ" for k by (intro sum_in_Reals real)
hence [simp]: "Im (?A k) = 0" for k by (auto elim!: Reals_cases)
have *: "Re (?A (p ^ m)) ≥ (if even m then 1 else 0)" if p: "prime p" for p m
proof -
have sum_neg1: "(∑i≤m. (-1) ^ i) = (if even m then 1 else (0::real))"
by (induction m) auto
from p have "?A (p ^ m) = (∑k≤m. χ (p ^ k))"
by (intro sum.reindex_bij_betw [symmetric] bij_betw_prime_power_divisors)
also have "Re … = (∑k≤m. Re (χ p) ^ k)" by (simp add: mult.power)
also have "… ≥ (if even m then 1 else 0)"
using sum_neg1 char_cases[of p] by (auto simp: power_0_left)
finally show ?thesis .
qed
have *: "Re (?A (p ^ m)) ≥ 0" "even m ⟹ Re (?A (p ^ m)) ≥ 1" if "prime p" for p m
using *[of p m] that by (auto split: if_splits)
have eq: "Re (?A k) = (∏p∈prime_factors k. Re (?A (p ^ multiplicity p k)))"
using k A by (subst sum.prod_prime_factors) (auto simp: Re_prod_Reals)
show "Re (∑d | d dvd k. χ d) ≥ 0" by (subst eq, intro prod_nonneg ballI *) auto
assume "is_square k"
then obtain m where m: "k = m ^ 2" by (auto elim!: is_nth_powerE)
have "even (multiplicity p k)" if "prime p" for p using k that unfolding m
by (subst prime_elem_multiplicity_power_distrib) (auto intro!: Nat.gr0I)
thus "Re (∑d | d dvd k. χ d) ≥ 1"
by (subst eq, intro prod_ge_1 ballI *) auto
qed
end
unbundle vec_lambda_notation
end