Theory Dirichlet_Theorem
section ‹Dirichlet's Theorem on primes in arithmetic progressions›
theory Dirichlet_Theorem
imports
Dirichlet_L_Functions
Bertrands_Postulate.Bertrand
Landau_Symbols.Landau_More
begin
text ‹
We can now turn to the proof of the main result: Dirichlet's theorem about the infinitude
of primes in arithmetic progressions.
There are previous proofs of this by John Harrison in HOL Light~\<^cite>‹"harrison-dirichlet"› and
by Mario Carneiro in Metamath~\<^cite>‹"carneiro16"›. Both of them strive to prove Dirichlet's
theorem with a minimum amount of auxiliary results and definitions, whereas our goal was to
get a short and simple proof of Dirichlet's theorem built upon a large library of Analytic
Number Theory.
At this point, we already have the key part -- the non-vanishing of $L(1,\chi)$
-- and the proof was relatively simple and straightforward due to the large amount of Complex
Analysis and Analytic Number Theory we have available. The remainder will be a bit more concrete,
but still reasonably concise.
First, we need to re-frame some of the results from the AFP entry about Bertrand's postulate a
little bit.
›
subsection ‹Auxiliary results›
text ‹
The AFP entry for Bertrand's postulate already provides a slightly stronger version of
this for integer values of $x$, but we can easily extend this to real numbers to obtain
a slightly nicer presentation.
›
lemma sum_upto_mangoldt_le:
assumes "x ≥ 0"
shows "sum_upto mangoldt x ≤ 3 / 2 * x"
proof -
have "sum_upto mangoldt x = psi (nat ⌊x⌋)"
by (simp add: sum_upto_altdef psi_def atLeastSucAtMost_greaterThanAtMost)
also have "… ≤ 551 / 256 * ln 2 * real (nat ⌊x⌋)"
by (rule psi_ubound_log)
also have "… ≤ 3 / 2 * real (nat ⌊x⌋)"
using Bertrand.ln_2_le by (intro mult_right_mono) auto
also have "… ≤ 3 / 2 * x" using assms by linarith
finally show ?thesis .
qed
text ‹
We can also, similarly, use the results from the Bertrand's postulate entry to show
that the sum of $\ln p / p$ over all primes grows logarithmically.
›
lemma Mertens_bigo:
"(λx. (∑p | prime p ∧ real p ≤ x. ln p / p) - ln x) ∈ O(λ_. 1)"
proof (intro bigoI[of _ 8] eventually_mono[OF eventually_gt_at_top[of 1]], goal_cases)
case (1 x)
have "¦(∑p | prime p ∧ p ≤ nat ⌊x⌋. ln p / p) - ln x¦ =
¦(∑p | prime p ∧ p ≤ nat ⌊x⌋. ln p / p) - ln (nat ⌊x⌋) - (ln x - ln (nat ⌊x⌋))¦"
by simp
also have "… ≤ ¦(∑p | prime p ∧ p ≤ nat ⌊x⌋. ln p / p) - ln (nat ⌊x⌋)¦ + ¦ln x - ln (nat ⌊x⌋)¦"
by (rule abs_triangle_ineq4)
also have "¦(∑p | prime p ∧ p ≤ nat ⌊x⌋. ln p / p) - ln (nat ⌊x⌋)¦ ≤ 7"
using 1 by (intro Mertens) auto
also have "¦ln x - ln (nat ⌊x⌋)¦ = ln x - ln (nat ⌊x⌋)"
using 1 by (intro abs_of_nonneg) auto
also from 1 have "… ≤ (x - nat ⌊x⌋) / nat ⌊x⌋" by (intro ln_diff_le) auto
also have "… ≤ (x - nat ⌊x⌋) / 1" using 1 by (intro divide_left_mono) auto
also have "… = x - nat ⌊x⌋" by simp
also have "… ≤ 1" using 1 by linarith
also have "(∑p | prime p ∧ p ≤ nat ⌊x⌋. ln p / p) = (∑p | prime p ∧ real p ≤ x. ln p / p)"
using 1 by (intro sum.cong refl) (auto simp: le_nat_iff le_floor_iff)
finally show ?case by simp
qed
subsection ‹The contribution of the non-principal characters›
text ‹
The estimates in the next two sections are partially inspired by John Harrison's
proof of Dirichlet's Theorem~\<^cite>‹"harrison-dirichlet"›.
We first estimate the growth of the partial sums of
\[-L'(1, \chi)/L(1, \chi) = \sum_{k=1}^\infty \chi(k) \frac{\Lambda(k)}{k}\]
for a non-principal character $\chi$ and show that they are, in fact, bounded, which is
ultimately a consequence of the non-vanishing of $L(1, \chi)$ for non-principal $\chi$.
›
context dcharacter
begin
context
includes no_vec_lambda_notation dcharacter_syntax
fixes L
assumes nonprincipal: "χ ≠ χ⇩0"
defines "L ≡ Dirichlet_L n χ 1"
begin
lemma Dirichlet_L_nonprincipal_mangoldt_bound_aux_strong:
assumes x: "x > 0"
shows "norm (L * sum_upto (λk. χ k * mangoldt k / k) x - sum_upto (λk. χ k * ln k / k) x)
≤ 9 / 2 * real (totient n)"
proof -
define B where "B = 3 * real (totient n)"
have "sum_upto (λk. χ k * ln k / k) x = sum_upto (λk. χ k * (∑d | d dvd k. mangoldt d) / k) x"
by (intro sum_upto_cong) (simp_all add: mangoldt_sum)
also have "… = sum_upto (λk. ∑d | d dvd k. χ k * mangoldt d / k) x"
by (simp add: sum_distrib_left sum_distrib_right sum_divide_distrib)
also have "… = sum_upto (λk. sum_upto (λd. χ (d * k) * mangoldt k / (d * k)) (x / real k)) x"
by (rule sum_upto_sum_divisors)
also have "… = sum_upto (λk. χ k * mangoldt k / k * sum_upto (λd. χ d / d) (x / real k)) x"
by (simp add: sum_upto_def sum_distrib_left mult_ac)
also have "L * sum_upto (λk. χ k * mangoldt k / k) x - … =
sum_upto (λk. (L - sum_upto (λd. χ d / d) (x / real k)) * (χ k * mangoldt k / k)) x"
unfolding ring_distribs by (simp add: sum_upto_def sum_subtractf sum_distrib_left mult_ac)
also have "norm … ≤ sum_upto (λk. B / x * mangoldt k) x" unfolding sum_upto_def
proof (rule sum_norm_le, goal_cases)
case (1 k)
have "norm ((L - sum_upto (λd. χ d / of_nat d) (x / k)) * χ k * (mangoldt k / of_nat k)) ≤
(B * real k / x) * 1 * (mangoldt k / real k)" unfolding norm_mult norm_divide
proof (intro mult_mono divide_left_mono)
show "norm (L - sum_upto (λd. χ d / d) (x / k)) ≤ B * real k / x"
using Dirichlet_L_minus_partial_sum_bound[OF nonprincipal, of 1 "x / k"] 1 x
by (simp add: powr_minus B_def L_def divide_simps norm_minus_commute)
qed (insert 1, auto intro!: divide_nonneg_pos mangoldt_nonneg norm_le_1 simp: B_def)
also have "… = B / x * mangoldt k" using 1 by simp
finally show ?case by (simp add: sum_upto_def mult_ac)
qed
also have "… = B / x * sum_upto mangoldt x"
unfolding sum_upto_def sum_distrib_left by simp
also have "… ≤ B / x * (3 / 2 * x)" using x
by (intro mult_left_mono sum_upto_mangoldt_le) (auto simp: B_def)
also have "… = 9 / 2 * real (totient n)" using x by (simp add: B_def)
finally show ?thesis by (simp add: B_def)
qed
lemma Dirichlet_L_nonprincipal_mangoldt_aux_bound:
"(λx. L * sum_upto (λk. χ k * mangoldt k / k) x - sum_upto (λk. χ k * ln k / k) x) ∈ O(λ_. 1)"
by (intro bigoI[of _ "9 / 2 * real (totient n)"] eventually_mono[OF eventually_gt_at_top[of 0]])
(use Dirichlet_L_nonprincipal_mangoldt_bound_aux_strong in simp_all)
lemma nonprincipal_mangoldt_bound:
"(λx. sum_upto (λk. χ k * mangoldt k / k) x) ∈ O(λ_. 1)" (is "?lhs ∈ _")
proof -
have [simp]: "L ≠ 0"
using nonprincipal unfolding L_def by (intro Dirichlet_L_Re_ge_1_nonzero_nonprincipal) auto
have "fds_converges (fds_deriv (fds χ)) 1" using conv_abscissa_le_0[OF nonprincipal]
by (intro fds_converges_deriv) (auto intro: le_less_trans)
hence "summable (λn. -(χ n * ln n / n))"
by (auto simp: fds_converges_def fds_deriv_def scaleR_conv_of_real fds_nth_fds' algebra_simps)
hence "summable (λn. χ n * ln n / n)" by (simp only: summable_minus_iff)
from summable_imp_convergent_sum_upto [OF this] obtain c where
"(sum_upto (λn. χ n * ln n / n) ⤏ c) at_top" by blast
hence *: "sum_upto (λk. χ k * ln k / k) ∈ O(λ_. 1)" unfolding sum_upto_def
by (intro bigoI_tendsto[of _ _ c]) auto
from sum_in_bigo[OF Dirichlet_L_nonprincipal_mangoldt_aux_bound *]
have "(λx. L * sum_upto (λk. χ k * mangoldt k / k) x) ∈ O(λ_. 1)" by (simp add: L_def)
thus ?thesis by simp
qed
end
end
subsection ‹The contribution of the principal character›
text ‹
Next, we turn to the analogous partial sum for the principal character and show that
it grows logarithmically and therefore is the dominant contribution.
›
context residues_nat
begin
context
includes no_vec_lambda_notation dcharacter_syntax
begin
lemma principal_dchar_sum_bound:
"(λx. (∑p | prime p ∧ real p ≤ x. χ⇩0 p * (ln p / p)) - ln x) ∈ O(λ_. 1)"
proof -
have fin [simp]: "finite {p. prime p ∧ real p ≤ x ∧ Q p}" for Q x
by (rule finite_subset[of _ "{..nat ⌊x⌋}"]) (auto simp: le_nat_iff le_floor_iff)
from fin[of _ "λ_. True"] have [simp]: "finite {p. prime p ∧ real p ≤ x}" for x
by (simp del: fin)
define P :: complex where "P = (∑p | prime p ∧ p dvd n. of_real (ln p / p))"
have "(λx. (∑p | prime p ∧ real p ≤ x. χ⇩0 p * (ln p / p)) - ln x) ∈
Θ(λx. of_real ((∑p | prime p ∧ real p ≤ x. ln p / p) - ln x) - P)" (is "_ ∈ Θ(?f)")
proof (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of "real n"]], goal_cases)
case (1 x)
have *: "{p. prime p ∧ real p ≤ x} =
{p. prime p ∧ real p ≤ x ∧ p dvd n} ∪ {p. prime p ∧ real p ≤ x ∧ ¬p dvd n}"
(is "_ = ?A ∪ ?B") by auto
have "(∑p | prime p ∧ real p ≤ x. of_real (ln p / p)) =
(∑p∈?A. of_real (ln p / p)) + (∑p∈?B. complex_of_real (ln p / p))"
by (subst *, subst sum.union_disjoint) auto
also from 1 have "?A = {p. prime p ∧ p dvd n}" using n by (auto dest: dvd_imp_le)
also have "(∑p∈…. of_real (ln p / p)) = P" by (simp add: P_def)
also have "(∑p∈?B. of_real (ln p / p)) =
(∑p | prime p ∧ real p ≤ x. χ⇩0 p * (ln p / p))"
by (intro sum.mono_neutral_cong_left)
(auto simp: principal_dchar_def prime_gt_0_nat coprime_absorb_left prime_imp_coprime)
finally show ?case using 1 by (simp add: Ln_of_real)
qed
also have "?f ∈ O(λ_. of_real 1)"
by (rule sum_in_bigo, subst landau_o.big.of_real_iff, rule Mertens_bigo) auto
finally show ?thesis by simp
qed
lemma principal_dchar_sum_bound':
"(λx. sum_upto (λk. χ⇩0 k * mangoldt k / k) x - Ln x) ∈ O(λ_. 1)"
proof -
have "(λx. sum_upto (λk. χ⇩0 k * mangoldt k / k) x -
(∑p | prime p ∧ real p ≤ x. χ⇩0 p * (ln p / p))) ∈ O(λ_. 1)"
proof (intro bigoI[of _ 3] eventually_mono[OF eventually_gt_at_top[of 0]], goal_cases)
case (1 x)
have "norm (complex_of_real (∑k | real k ≤ x ∧ coprime k n. mangoldt k / k) -
of_real (∑p | prime p ∧ p ∈ {k. real k ≤ x ∧ coprime k n}. ln p / p)) ≤ 3"
unfolding of_real_diff [symmetric] norm_of_real
by (rule Mertens_mangoldt_versus_ln[where n = "nat ⌊x⌋"])
(insert n, auto simp: Suc_le_eq le_nat_iff le_floor_iff intro!: Nat.gr0I)
also have "complex_of_real (∑k | real k ≤ x ∧ coprime k n. mangoldt k / k) =
sum_upto (λk. χ⇩0 k * mangoldt k / k) x"
unfolding sum_upto_def of_real_sum using n
by (intro sum.mono_neutral_cong_left) (auto simp: principal_dchar_def intro!: Nat.gr0I)
also have "complex_of_real (∑p | prime p ∧ p ∈ {k. real k ≤ x ∧ coprime k n}. ln p / p) =
(∑p | prime p ∧ real p ≤ x. χ⇩0 p * (ln p / p))"
unfolding of_real_sum
by (intro sum.mono_neutral_cong_left)
(auto simp: principal_dchar_def le_nat_iff le_floor_iff prime_gt_0_nat
intro!: finite_subset[of _ "{..nat ⌊x⌋}"])
finally show ?case by simp
qed
from sum_in_bigo(1)[OF principal_dchar_sum_bound this] show ?thesis
by simp
qed
subsection ‹The main result›
text ‹
We can now show the main result by extracting the primes we want using the orthogonality
relation on characters, separating the principal part of the sum from the non-principal ones
and then applying the above estimates.
›
lemma Dirichlet_strong:
assumes "coprime h n"
shows "(λx. (∑p | prime p ∧ [p = h] (mod n) ∧ real p ≤ x. ln p / p) - ln x / totient n)
∈ O(λ_. 1)" (is "(λx. sum _ (?A x) - _) ∈ _")
proof -
from assms obtain h' where h': "[h * h' = Suc 0] (mod n)"
by (subst (asm) coprime_iff_invertible_nat) blast
let ?A' = "λx. {p. p > 0 ∧ real p ≤ x ∧ [p = h] (mod n)}"
let ?B = "dcharacters n - {χ⇩0}"
have [simp]: "χ⇩0 ∈ dcharacters n"
by (auto simp: dcharacters_def principal.dcharacter_axioms)
have "(λx. of_nat (totient n) * (∑p∈?A' x. mangoldt p / p) - ln x) ∈
Θ(λx. sum_upto (λk. χ⇩0 k * mangoldt k / k) x - ln x +
(∑χ∈?B. χ h' * sum_upto (λk. χ k * mangoldt k / k) x))"
(is "_ ∈ Θ(?f)")
proof (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 0]], goal_cases)
case (1 x)
have "of_nat (totient n) * (∑p∈?A' x. of_real (mangoldt p / p) :: complex) =
(∑p∈?A' x. of_nat (totient n) * of_real (mangoldt p / p))"
by (subst sum_distrib_left) simp_all
also have "… = sum_upto (λk. ∑χ∈dcharacters n. χ (h' * k) * (mangoldt k / k)) x"
unfolding sum_upto_def
proof (intro sum.mono_neutral_cong_left ballI, goal_cases)
case (3 p)
have "[h' * p ≠ 1] (mod n)"
proof
assume "[h' * p = 1] (mod n)"
hence "[h * (h' * p) = h * 1] (mod n)" by (rule cong_scalar_left)
hence "[h = h * h' * p] (mod n)" by (simp add: mult_ac cong_sym)
also have "[h * h' * p = 1 * p] (mod n)"
using h' by (intro cong_scalar_right) auto
finally have "[p = h] (mod n)" by (simp add: cong_sym)
with 3 show False by auto
qed
thus ?case
by (auto simp: sum_dcharacters sum_divide_distrib [symmetric] sum_distrib_right [symmetric])
next
case (4 p)
hence "[p * h' = h * h'] (mod n)" by (intro cong_scalar_right) auto
also have "[h * h' = 1] (mod n)" using h' by simp
finally have "[h' * p = 1] (mod n)" by (simp add: mult_ac)
thus ?case using h' 4
by (auto simp: sum_dcharacters sum_divide_distrib [symmetric] sum_distrib_right [symmetric])
qed auto
also have "… = (∑χ∈dcharacters n. sum_upto (λk. χ (h' * k) * (mangoldt k / k)) x)"
unfolding sum_upto_def by (rule sum.swap)
also have "… = (∑χ∈dcharacters n. χ h' * sum_upto (λk. χ k * (mangoldt k / k)) x)"
unfolding sum_upto_def
by (intro sum.cong refl) (auto simp: dcharacters_def dcharacter.mult sum_distrib_left mult_ac)
also have "… = χ⇩0 h' * sum_upto (λk. χ⇩0 k * (mangoldt k / k)) x +
(∑χ∈?B. χ h' * sum_upto (λk. χ k * (mangoldt k / k)) x)"
by (subst sum.remove [symmetric]) (auto simp: sum_distrib_left)
also have "coprime h' n"
using h' by (subst coprime_iff_invertible_nat, subst (asm) mult.commute) auto
hence "χ⇩0 h' = 1"
by (simp add: principal_dchar_def)
finally show ?case using n 1 by (simp add: Ln_of_real)
qed
also have "?f ∈ O(λ_. complex_of_real 1)"
proof (rule sum_in_bigo[OF _ big_sum_in_bigo], goal_cases)
case 1
from principal_dchar_sum_bound' show ?case by simp
next
case (2 χ)
then interpret dcharacter n G χ by (simp_all add: G_def dcharacters_def)
from 2 have "χ ≠ χ⇩0" by auto
thus ?case unfolding of_real_1
by (intro landau_o.big.mult_in_1 nonprincipal_mangoldt_bound) auto
qed
finally have *: "(λx. real (totient n) * (∑p∈?A' x. mangoldt p / p) - ln x) ∈ O(λ_. 1)"
by (subst (asm) landau_o.big.of_real_iff)
have "(λx. real (totient n) * ((∑p∈?A x. ln p / p) - (∑p∈?A' x. mangoldt p / p))) ∈ O(λ_. 1)"
proof (intro landau_o.big.mult_in_1)
show "(λx. (∑p∈?A x. ln p / p) - (∑p∈?A' x. mangoldt p / p)) ∈ O(λ_. 1)"
unfolding landau_o.big.of_real_iff
proof (intro bigoI[of _ 3] eventually_mono[OF eventually_gt_at_top[of 0]], goal_cases)
case (1 x)
have "¦(∑p∈?A' x. mangoldt p / p) - (∑p | prime p ∧ p ∈ ?A' x. ln p / p)¦ ≤ 3"
by (rule Mertens_mangoldt_versus_ln[where n = "nat ⌊x⌋"])
(auto simp: le_nat_iff le_floor_iff)
also have "{p. prime p ∧ p ∈ ?A' x} = ?A x" by (auto simp: prime_gt_0_nat)
finally show ?case by (simp add: abs_minus_commute)
qed
qed auto
from sum_in_bigo(1)[OF * this]
have "(λx. totient n * (∑p∈?A x. ln p / p) - ln x) ∈ O(λ_. 1)"
by (simp add: field_simps)
also have "(λx. totient n * (∑p∈?A x. ln p / p) - ln x) =
(λx. totient n * ((∑p∈?A x. ln p / p) - ln x / totient n))"
using n by (intro ext) (auto simp: field_simps)
also have "… ∈ O(λ_. 1) ⟷ ?thesis" using n
by (intro landau_o.big.cmult_in_iff) auto
finally show ?thesis .
qed
text ‹
It is now obvious that the set of primes we are interested in is, in fact, infinite.
›
theorem Dirichlet:
assumes "coprime h n"
shows "infinite {p. prime p ∧ [p = h] (mod n)}"
proof
assume "finite {p. prime p ∧ [p = h] (mod n)}"
then obtain K where K: "{p. prime p ∧ [p = h] (mod n)} ⊆ {..<K}"
by (auto simp: finite_nat_iff_bounded)
have "eventually (λx. (∑p | prime p ∧ [p = h] (mod n) ∧ real p ≤ x. ln p / p) =
(∑p | prime p ∧ [p = h] (mod n). ln p / p)) at_top"
using eventually_ge_at_top[of "real K"] by eventually_elim (intro sum.cong, use K in auto)
hence "(λx. (∑p | prime p ∧ [p = h] (mod n) ∧ real p ≤ x. ln p / p)) ∈
Θ(λ_. (∑p | prime p ∧ [p = h] (mod n). ln p / p))" by (intro bigthetaI_cong) auto
also have "(λ_. (∑p | prime p ∧ [p = h] (mod n). ln p / p)) ∈ O(λ_. 1)" by simp
finally have "(λx. (∑p | prime p ∧ [p = h] (mod n) ∧ real p ≤ x. ln p / p)) ∈ O(λ_. 1)" .
from sum_in_bigo(2)[OF this Dirichlet_strong[OF assms]] and n show False by simp
qed
text ‹
In the future, one could extend this result to more precise estimates of the distribution
of primes in arithmetic progressions in a similar way to the Prime Number Theorem.
›
end
end
end