The real Euler product of the Dedekind zeta function in exponential form

For real s > 1, every local ratio x = N(𝔭) ^ (-s) of a height-one prime lies in (0, 1/2], because N(𝔭) ≥ 2. The principal logarithm of each Euler factor is then the real number -log (1 - x), and the exponential form TauCeti.MultiplicativeIdealWeight.exp_tsum_neg_log_one_sub_eq_LSeries of the Euler product, specialized to the trivial weight, becomes a statement about real numbers: ζ_K(s) is the exponential of the convergent real sum ∑_𝔭 -log (1 - N(𝔭) ^ (-s)). In particular ζ_K(s) is a positive real number, and that sum is its real logarithm.

Main results

• IsDedekindDomain.HeightOneSpectrum.absNorm_rpow_neg_le_half: N(𝔭) ^ (-s) ≤ 1/2 for 1 ≤ s.
• TauCeti.summable_neg_log_one_sub_absNorm_rpow: ∑_𝔭 -log (1 - N(𝔭) ^ (-s)) converges for 1 < s.
• TauCeti.dedekindZeta_ofReal_eq_exp_tsum_neg_log_one_sub: for real s > 1, ζ_K(s) is the exponential of that real sum.
• TauCeti.dedekindZeta_re_eq_exp and TauCeti.dedekindZeta_re_pos: the same for the real part, which is therefore positive.
• TauCeti.log_dedekindZeta_re_eq_tsum_neg_log_one_sub: that real sum is the real logarithm of ζ_K(s).

References

• The real logarithmic identity also appears, under the same name, in the Birkbeck–Brasca Chebotarev density project, https://github.com/CBirkbeck/chebotarev-density (Apache-2.0), commit 8575c9df1ae0a61120ab5c964c7911414254bec7, file CebotarevDensity/Density.lean, where it is proved from Real.hasProd_of_hasSum_log and the product formula. It is derived here instead from TauCeti's exponential Euler product TauCeti.MultiplicativeIdealWeight.exp_tsum_neg_log_one_sub_eq_LSeries.

theorem IsDedekindDomain.HeightOneSpectrum.absNorm_rpow_neg_le_half {K : Type u_1} [Field K] [NumberField K] (P : HeightOneSpectrum (NumberField.RingOfIntegers K)) {s : ℝ} (hs : 1 ≤ s) : ↑(Ideal.absNorm P.asIdeal) ^ (-s) ≤ 1 / 2

For 1 ≤ s, the local ratio N(𝔭) ^ (-s) of a height-one prime is at most 1/2, because N(𝔭) ≥ 2.

theorem TauCeti.summable_neg_log_one_sub_absNorm_rpow {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : Summable fun (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => -Real.log (1 - ↑(Ideal.absNorm P.asIdeal) ^ (-s))

For 1 < s, the real logarithms -log (1 - N(𝔭) ^ (-s)) of the Euler factors of the Dedekind zeta function are summable over the height-one primes.

theorem TauCeti.dedekindZeta_ofReal_eq_exp_tsum_neg_log_one_sub {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : NumberField.dedekindZeta K ↑s = ↑(Real.exp (∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), -Real.log (1 - ↑(Ideal.absNorm P.asIdeal) ^ (-s))))

The real Euler product of the Dedekind zeta function in exponential form. For real s > 1, ζ_K(s) is the exponential of the convergent real sum ∑_𝔭 -log (1 - N(𝔭) ^ (-s)) over the height-one primes of 𝓞 K. In particular ζ_K(s) is a positive real number, and that sum is its real logarithm.

This is TauCeti.MultiplicativeIdealWeight.exp_tsum_neg_log_one_sub_eq_LSeries for the trivial weight, with each principal logarithm identified with a real one.

theorem TauCeti.dedekindZeta_re_eq_exp {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : (NumberField.dedekindZeta K ↑s).re = Real.exp (∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), -Real.log (1 - ↑(Ideal.absNorm P.asIdeal) ^ (-s)))

For real s > 1, the real part of ζ_K(s) is the exponential of ∑_𝔭 -log (1 - N(𝔭) ^ (-s)).

theorem TauCeti.log_dedekindZeta_re_eq_tsum_neg_log_one_sub {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : Real.log (NumberField.dedekindZeta K ↑s).re = ∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), -Real.log (1 - ↑(Ideal.absNorm P.asIdeal) ^ (-s))

The real logarithm of the Dedekind zeta function. For real s > 1, the real logarithm of ζ_K(s) is the convergent sum ∑_𝔭 -log (1 - N(𝔭) ^ (-s)) over the height-one primes of 𝓞 K.

theorem TauCeti.dedekindZeta_re_pos {K : Type u_1} [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : 0 < (NumberField.dedekindZeta K ↑s).re

For real s > 1, the real part of ζ_K(s) is positive.