Documentation

TauCeti.NumberTheory.LFunctions.Mertens

Mertens' theorems for a number field #

Let K be a number field. This file proves Mertens' first theorem for K: the sum of log N𝔭 / N𝔭 over the nonzero prime ideals 𝔭 of 𝓞 K of norm at most x is log x + O(1). Over ℚ this is Mertens' classical estimate ∑_{p ≤ x} log p / p = log x + O(1). Partial summation then gives Mertens' second theorem, ∑_{N𝔭 ≤ x} 1 / N𝔭 = log log x + B_K + O(1 / log x) with a constant B_K. Identifying B_K through the Euler product of ζ_K gives Mertens' product (Rosen) ∏_{N𝔭 ≤ x} (1 - N𝔭⁻¹)⁻¹ ~ e^γ κ_K log x, with γ Euler's constant and κ_K the residue of ζ_K at s = 1. Over ℚ this is Mertens' third theorem ∏_{p ≤ x} (1 - 1 / p)⁻¹ ~ e^γ log x.

The proof of the first theorem evaluates ∑_{N𝔞 ≤ x} log N𝔞 in two ways.

Inserting the ideal count into the first expression produces the main term κ_K x ∑_{N𝔟 ≤ x} Λ_K(𝔟) / N𝔟. The error terms sum to O(x ^ (1 - 1 / [K : ℚ]) ∑_{N𝔟 ≤ x} Λ_K(𝔟) N𝔟 ^ (1 / [K : ℚ] - 1)), which partial summation from Chebyshev's bound ψ_K(t) = O(t) (a consequence of TauCeti.primeIdealTheorem) makes O(x). Dividing by κ_K x, with κ_K = dedekindZeta_residue K > 0, gives the prime-power form ∑_{N𝔟 ≤ x} Λ_K(𝔟) / N𝔟 = log x + O(1). The higher prime powers 𝔭 ^ k, k ≥ 2, contribute O(1), because their weighted count is O(√t log² t) (TauCeti.higherPrimePowerTheta_le).

For the second theorem, write S(t) = ∑_{N𝔭 ≤ t} log N𝔭 / N𝔭 = log t + R(t), so that R is bounded on t ≥ 2 by the first theorem. Abel summation against 1 / log t (TauCeti.primeSummatory_div_log_eq_div_log_add_integral) gives ∑_{N𝔭 ≤ x} 1 / N𝔭 = S(x) / log x + ∫_2^x S(t) / (t log² t) dt. The main part log t of S integrates to log log x - log log 2, and ∫_2^∞ R(t) / (t log² t) dt converges absolutely with tail O(1 / log x) beyond x. The resulting expansion is that of Lebacque, Proposition 2.

For the product, the constant B_K is computed from the behaviour of the prime zeta sum P(s) = ∑_𝔭 N𝔭 ^ (-s) as s → 1⁺ (Lebacque, Proposition 3). Abel summation writes P(s) = (s - 1) ∫_1^∞ t ^ (-s) (∑_{N𝔭 ≤ t} 1 / N𝔭) dt. The second theorem and the Abelian limit TauCeti.tendsto_smul_integral_Ioi_rpow_smul_nhdsGT_zero handle the part ∑_{N𝔭 ≤ t} 1 / N𝔭 - log log t → B_K. Mathlib's Real.eulerMascheroniConstant_eq_neg_integral_log_log evaluates the log log t part exactly: (s - 1) ∫_1^∞ log (log t) t ^ (-s) dt = -γ - log (s - 1). Together they give P(s) = log (1 / (s - 1)) + B_K - γ + o(1). On the other side, the Euler product writes log ζ_K(s) as P(s) plus the sum of the remainders -log (1 - N𝔭 ^ (-s)) - N𝔭 ^ (-s). That sum is continuous at s = 1 (TauCeti.tendsto_tsum_neg_log_one_sub_sub_absNorm_rpow), and the residue gives log ζ_K(s) = log (1 / (s - 1)) + log κ_K + o(1). Comparing the two expansions gives B_K = γ + log κ_K + ∑_𝔭 (log (1 - N𝔭⁻¹) + N𝔭⁻¹). Adding the convergent sum of the remainders at s = 1 to the second theorem then gives the logarithm of the product.

Main results #

References #

Chebyshev's identity #

source
theorem TauCeti.LFunctions.idealSummatory_log_absNorm_eq (K : Type u_1) [Field K] [NumberField K] (x : ℝ) :
idealSummatory K (fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => Real.log ↑(Ideal.absNorm ↑I)) x = primePowerSummatory K (fun (A : IdealPrimePower K) => primePowerWeight A * ↑(idealsLE K (x / ↑(Ideal.absNorm ↑↑A))).card) x

Chebyshev's identity for a number field. Summing log N𝔞 = ∑_{𝔟 ∣ 𝔞} Λ_K(𝔟) over the nonzero integral ideals of norm at most x and exchanging the order of summation, ∑_{N𝔞 ≤ x} log N𝔞 = ∑_{N(𝔭 ^ k) ≤ x} log N𝔭 · #{𝔞 : N𝔞 ≤ x / N(𝔭 ^ k)}.

Uniform forms of the two counting estimates #

Mertens' first theorem #

source
theorem TauCeti.LFunctions.isBigO_primePowerSummatory_div_sub_log (K : Type u_1) [Field K] [NumberField K] :
(fun (x : ℝ) => primePowerSummatory K (fun (A : IdealPrimePower K) => primePowerWeight A / ↑(Ideal.absNorm ↑↑A)) x - Real.log x) =O[Filter.atTop] fun (x : ℝ) => 1

Mertens' first theorem for a number field, prime-power form. The sum of Λ_K(𝔞) / N𝔞 over the nonzero integral ideals of norm at most x is log x + O(1): the weight log N𝔭 of each prime power 𝔭 ^ k divided by its norm, summed over N(𝔭 ^ k) ≤ x, differs from log x by a bounded amount.

source
theorem TauCeti.LFunctions.isBigO_primeSummatory_log_absNorm_div_sub_log (K : Type u_1) [Field K] [NumberField K] :
(fun (x : ℝ) => primeSummatory K (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => Real.log ↑(Ideal.absNorm v.asIdeal) / ↑(Ideal.absNorm v.asIdeal)) x - Real.log x) =O[Filter.atTop] fun (x : ℝ) => 1

Mertens' first theorem for a number field. The sum of log N𝔭 / N𝔭 over the nonzero prime ideals 𝔭 of 𝓞 K of norm at most x is log x + O(1).

Mertens' second theorem #

source
noncomputable def TauCeti.LFunctions.mertensConstant (K : Type u_1) [Field K] [NumberField K] :
ℝ

Mertens' constant of a number field: the limit B_K of ∑_{N𝔭 ≤ x} 1 / N𝔭 - log log x as x → ∞, the sum over the nonzero prime ideals of 𝓞 K. It exists by tendsto_primeSummatory_inv_absNorm_sub_log_log; over ℚ it is the classical Meissel–Mertens constant.

Instances For
    source
    theorem TauCeti.LFunctions.isBigO_primeSummatory_inv_absNorm_sub_log_log_sub_mertensConstant (K : Type u_1) [Field K] [NumberField K] :
    (fun (x : ℝ) => primeSummatory K (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => (↑(Ideal.absNorm v.asIdeal))⁻¹) x - Real.log (Real.log x) - mertensConstant K) =O[Filter.atTop] fun (x : ℝ) => (Real.log x)⁻¹

    Mertens' second theorem for a number field. The sum of 1 / N𝔭 over the nonzero prime ideals 𝔭 of 𝓞 K of norm at most x is log log x + B_K + O(1 / log x), where B_K = mertensConstant K.

    source
    theorem TauCeti.LFunctions.tendsto_primeSummatory_inv_absNorm_sub_log_log (K : Type u_1) [Field K] [NumberField K] :
    Filter.Tendsto (fun (x : ℝ) => primeSummatory K (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => (↑(Ideal.absNorm v.asIdeal))⁻¹) x - Real.log (Real.log x)) Filter.atTop (nhds (mertensConstant K))

    Mertens' second theorem for a number field, limit form. As x → ∞, ∑_{N𝔭 ≤ x} 1 / N𝔭 - log log x tends to Mertens' constant B_K = mertensConstant K.

    Mertens' product #

    source
    theorem TauCeti.LFunctions.tendsto_primeIdealZetaSum_univ_sub_log_one_div_sub_one (K : Type u_1) [Field K] [NumberField K] :
    Filter.Tendsto (fun (s : ℝ) => NumberField.Set.primeIdealZetaSum Set.univ s - Real.log (1 / (s - 1))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (mertensConstant K - Real.eulerMascheroniConstant))

    The prime zeta sum near s = 1, with its constant. As s → 1⁺, ∑_𝔭 N𝔭 ^ (-s) = log (1 / (s - 1)) + B_K - γ + o(1), where B_K = mertensConstant K and γ is Euler's constant. This refines TauCeti.primeIdealZetaSum_univ_sub_log_one_div_sub_one_isBigO, which bounds the difference by a constant.

    source
    theorem TauCeti.LFunctions.mertensConstant_eq (K : Type u_1) [Field K] [NumberField K] :
    mertensConstant K = Real.eulerMascheroniConstant + Real.log (NumberField.dedekindZeta_residue K) + ∑' (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (Real.log (1 - (↑(Ideal.absNorm v.asIdeal))⁻¹) + (↑(Ideal.absNorm v.asIdeal))⁻¹)

    Mertens' constant of a number field in closed form (Rosen; Lebacque, Proposition 3): B_K = γ + log κ_K + ∑_𝔭 (log (1 - N𝔭⁻¹) + N𝔭⁻¹), with γ Euler's constant and κ_K = dedekindZeta_residue K the residue of ζ_K at s = 1. Over ℚ this is the classical expression of the Meissel–Mertens constant.

    source
    theorem TauCeti.LFunctions.tendsto_primeSummatory_neg_log_one_sub_inv_absNorm_sub_log_log (K : Type u_1) [Field K] [NumberField K] :
    Filter.Tendsto (fun (x : ℝ) => primeSummatory K (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => -Real.log (1 - (↑(Ideal.absNorm v.asIdeal))⁻¹)) x - Real.log (Real.log x)) Filter.atTop (nhds (Real.eulerMascheroniConstant + Real.log (NumberField.dedekindZeta_residue K)))

    Mertens' product for a number field, logarithmic form. As x → ∞, ∑_{N𝔭 ≤ x} -log (1 - N𝔭⁻¹) = log log x + γ + log κ_K + o(1), the sum over the nonzero prime ideals of 𝓞 K of norm at most x, with γ Euler's constant and κ_K = dedekindZeta_residue K.

    source
    theorem TauCeti.LFunctions.tendsto_prod_one_sub_inv_absNorm_div_log (K : Type u_1) [Field K] [NumberField K] :
    Filter.Tendsto (fun (x : ℝ) => (∏ᶠ (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), if ↑(Ideal.absNorm 𝔭.asIdeal) ≤ x then (1 - (↑(Ideal.absNorm 𝔭.asIdeal))⁻¹)⁻¹ else 1) / (Real.exp Real.eulerMascheroniConstant * NumberField.dedekindZeta_residue K * Real.log x)) Filter.atTop (nhds 1)

    Mertens' product for a number field (Rosen; Lebacque, Generalised Mertens and Brauer–Siegel theorems, Theorem 5 (NF)): as x → ∞, ∏_{N𝔭 ≤ x} (1 - N𝔭⁻¹)⁻¹ ~ e^γ κ_K log x, the product over the nonzero prime ideals of 𝓞 K of absolute norm at most x, with γ Euler's constant and κ_K = dedekindZeta_residue K the residue of ζ_K at s = 1. The factor is 1 at every prime of norm above x, so the product is a finprod. Over ℚ it is Mertens' third theorem ∏_{p ≤ x} (1 - 1 / p)⁻¹ ~ e^γ log x.