FC09 — Jürgen Neukirch, Algebraic Number Theory (1999)

FC09 — Neukirch, Algebraic Number Theory.

This chapter contains 55 definitions, 15 theorems, 47 propositions, 12 lemmas, 18 corollaries, 21 conventions and 7 other statements.

Of the 175 statements checked against Lean, 28 are formalized somewhere and 147 are not.

Status	Statements	Share	What it means
not formalized	147	84%	A documented search found no Lean statement of it anywhere.
in Mathlib	25	14%	Mathlib states and proves it.
in another Lean project	3	2%	Some other Lean development has it; using it means porting that code.
checked in total	175

Which versions of Lean and Mathlib were searched

Canonical source block: FC09 Neukirch Chapter VII, “Zeta Functions and L-series”, FC09-C07-U001–FC09-C07-U175, in canonical source-ID order from Foundational corpus units FC09 Neukirch. The generator retrieves all 175 rows through agent-memory, asserts exact order/uniqueness, and assigns exactly one route to every unit. C07 is the final FC09 chapter in the canonical catalogue.
Project-first inspection used A=3b2239e161592472b34e02ad3b7da308f9ce7280 (Lean 4.33.0, Apache-2.0). The project has lattice theta/formal-series material but no additional analytic number theory interface that closes a C07 row; therefore C07 has no project-existing route.
Pinned Mathlib is P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native coverage is concentrated in the classical analytic substrate: Riemann zeta and its completion, complex Gamma, theta/Hurwitz kernels and abstract Mellin functional equations, Bernoulli/zeta special values, Dirichlet characters and L-series/Euler products, Schwartz Fourier theory, Dedekind zeta, Dirichlet nonvanishing/primes in progressions, representation characters, and Dirichlet density. Uniform convergence in U001/U008/U018 is credited only after the checked summable majorants are combined with Mathlib’s uniform M-test.
Current Mathlib was checked at H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. It adds no source-complete general Artin-L, Chebotarev, or global Hecke analytic layer closing the unmatched C07 blocks. Open PR #40736 was inspected at O=945b7b641bcfd4b2b787a8abf241fdb65ad70dc1: it defines a number-field HeckeCharacter as an algebraic MulChar of the idèle class group and defines local Euler factors/L-functions, but it does not impose Neukirch’s required continuity into S¹ or prove the Hecke analytic theory, so it earns no row here.
External analytic discovery found CBirkbeck/AINTLIB@160e446617a2168c34c95bbe7a76c4105b392434 (Apache-2.0; Mathlib pin e4b72ca0d01c5f45c485814ec129debbc4f64634). Its DedekindResidue Poisson development is sorry-free in the cited files and proves the full GL Fourier change-of-variables formula, the n-dimensional Gaussian transform, dual lattices and lattice Poisson summation. These are conservatively reference-port routes for U039–U040 because the package is on a distinct Mathlib revision; for U040 the external Poisson theorem’s summability hypotheses are discharged for Schwartz maps by pinned rapid-decay seminorms and ZLattice.summable_norm_rpow.
External discovery also found Vilin97/lean-pool@c8ddda0a64f21cb019720cdda48c94354d4091e7 (Apache-2.0; Mathlib pin de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11), whose sorry-free Dedekind-zeta files prove the literal ideal series, prime-ideal Euler product and locally uniform product control. Combined with the pinned uniform M-test this closes U053 as a reference-port. AINTLIB additionally has a general completed-Dedekind-zeta functional equation, but Neukirch U064–U065 bundle exact residue/normalization assertions not exported as one checked theorem, so strict bundle semantics leaves them unmatched. AINTLIB’s cyclotomic zeta factorization currently treats prime conductor p, not Neukirch’s arbitrary m, so U066 also remains unmatched.
Chebotarev-specific discovery checked CBirkbeck/chebotarev-density@c64095e6cc6483b401849c7fd9182d983d3bf261 (Apache-2.0; Mathlib pin e568743e9c24da15c8f8347a47931d2a6c33ff85), but its named chebotarev_density theorem still contains sorry; TauCeti supplies substantial Frobenius-prime/counting infrastructure but not the density theorem itself. No Chebotarev row is credited.
Strict bundle semantics was enforced across all 13 sections. A functional equation without the source’s root-number modulus, residue normalization or special-value formula does not earn the row; generic finite-group induction does not earn Brauer/character-basis assertions; the algebraic Hecke-character PR does not earn continuous Größencharacters; and Frobenius or density definitions do not earn prime-density theorems.
Short derivations are credited only where the checked APIs close the whole source unit: Gamma residues at -n follow from the residue at zero plus recurrence; negative-half-plane zeta zero classification follows from the functional equation, Gamma nonvanishing and right-half-plane nonvanishing; and the uniform half-plane convergence rows use explicit summable majorants plus the library M-test.
All mathlib targets were path/token validated against P, every external positive target was checked at its exact repository revision with sorry/*_wanted excluded in the cited files, and current/open/external negative boundaries were rechecked against H, PR #40736 and the Chebotarev/cyclotomic candidates.
Route totals for C07: mathlib 25, project-existing 0, package-import 0, reference-port 3, unmatched 147.

Proposition (1.1)

FC09-C07-U001 · Chapter VII, §1, source L17609 · in Mathlib

(1.1) Proposition. The series \(\zeta(s) = \sum_{n=1}^{\infty} \frac{1}{n^s}\) is absolutely and uniformly convergent in the domain \(\operatorname{Re}(s) \geq 1 + \delta\) , for every \(\delta > 0\) . It therefore represents an analytic function in the half-plane \(\operatorname{Re}(s) > 1\) . One has Euler’s identity \[ \zeta (s) = \prod_ {p} \frac {1}{1 - p ^ {- s}}, \] where p runs through the prime numbers.

Formalized. Mathlib/NumberTheory/LSeries/Dirichlet.lean::LSeriesSummable_zeta_iff, LSeries_zeta_eq_riemannZeta; Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean::riemannZeta_eulerProduct; Mathlib/Analysis/Normed/Group/FunctionSeries.lean::tendstoUniformlyOn_tsum — The zeta coefficient series is summable exactly for Re(s)>1 and equals riemannZeta; the Euler-product theorem is exact. On Re(s)≥1+δ, the terms are uniformly dominated by n^-(1+δ), so Mathlib’s uniform M-test supplies Neukirch’s stated uniform convergence and hence analyticity.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U002 · Chapter VII, §1, source L17669 · in Mathlib

Euler’s identity expresses the law of unique prime factorization of natural numbers in a single equation. This already demonstrates the number-theoretic significance of the zeta function. It challenges us to study its properties more closely. By its definition, the function is only given on the half-plane \(\operatorname{Re}(s) > 1\) . It does, however, admit an analytic continuation to the whole complex plane, with the point \(s = 1\) removed, and it satisfies a functional equation which relates the argument \(s\) to the argument \(1 - s\) . These crucial facts will be proved next. The proof hinges on an integral formula for the zeta function \(\zeta(s)\) which arises from the well-known gamma function. This latter is defined for \(\operatorname{Re}(s) > 0\) by the absolutely convergent integral \[ \Gamma (s) = \int_ {0} ^ {\infty} e ^ {- y} y ^ {s} \frac {d y}{y} \] and obeys the following rules (see [34], vol. I, chap. I).

Formalized. Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean::GammaIntegral, Gamma_eq_integral; Mathlib/NumberTheory/LSeries/RiemannZeta.lean::riemannZeta_one_sub, analyticOn_riemannZeta — For Re(s)>0, Gamma_eq_integral identifies Gamma with the Euler integral. The same pinned Riemann-zeta file already supplies the continuation and functional equation whose derivation Neukirch introduces from this integral.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (1.2)

FC09-C07-U003 · Chapter VII, §1, source L17677 · in Mathlib

(1.2) Proposition. (i) The gamma function is analytic and admits a meromorphic continuation to all of \(\mathbb{C}\) . (ii) It is nowhere zero and has simple poles at \(s = -n\) , \(n = 0, 1, 2, \ldots\) , with residues \((-1)^n / n!\) . There are no poles anywhere else. (iii) It satisfies the functional equations 1) \(\Gamma(s + 1) = s\Gamma(s)\) , 2) \(\Gamma(s)\Gamma(1 - s) = \frac{\pi}{\sin\pi s},\) 3) \(\Gamma(s)\Gamma(s + \frac{1}{2}) = \frac{2\sqrt{\pi}}{2^{2s}}\Gamma(2s)\) (Legendre’s duplication formula). (iv) It has the special values \(\Gamma(1/2) = \sqrt{\pi}\) , \(\Gamma(1) = 1\) , \(\Gamma(k+1) = k!\) , \(k = 0, 1, 2, \ldots\) .

Formalized. Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean::Gamma_eq_integral, Gamma_add_one, Gamma_nat_eq_factorial, Gamma_ne_zero; Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean::differentiableAt_Gamma, tendsto_self_mul_Gamma_nhds_zero; Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean::Gamma_mul_Gamma_one_sub, Gamma_mul_Gamma_add_half; Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean::Gamma_one_half_eq — Pinned Mathlib proves analyticity away from the nonpositive integers, nonvanishing there, recurrence, reflection, duplication, Γ(1/2)=√π and factorial values. The residue 1 at 0 is tendsto_self_mul_Gamma_nhds_zero; recurrence gives residue (-1)^n/n! at -n and shows these are the only simple poles.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U004 · Chapter VII, §1, source L17721 · in Mathlib

The function \[ Z(s) = \pi^{-s/2}\Gamma(s/2)\zeta(s) \] is called the completed zeta function; its integral representation is proposition (1.3).

Formalized. Mathlib/NumberTheory/LSeries/RiemannZeta.lean::completedRiemannZeta, completedZeta_eq_tsum_of_one_lt_re — completedRiemannZeta is the completed zeta with the same π/Gamma normalization (equivalently Mathlib’s Γℝ normalization), and the convergence-range formula recovers π^{-s/2} Γ(s/2) ζ(s).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (1.3)

FC09-C07-U005 · Chapter VII, §1, source L17729 · in Mathlib

(1.3) Proposition. The completed zeta function \(Z(s)\) admits the integral representation \[ Z (s) = \frac {1}{2} \int_ {0} ^ {\infty} (\theta (i y) - 1) y ^ {s / 2} \frac {d y}{y}. \]

Formalized. Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean::evenKernel_def, hasSum_int_evenKernel, hurwitzEvenFEPair, hasSum_int_completedHurwitzZetaEven; Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean::WeakFEPair.hasMellin — At parameter a=0, the even Hurwitz kernel is the classical theta sum. Its FEPair Mellin formula, after subtracting the constant term and changing s↦s/2, is exactly the half-integral representation of completed Riemann zeta used by Neukirch.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U006 · Chapter VII, §1, source L17735 · in Mathlib

The proof of the functional equation for the function \(Z(s)\) is based on the following general principle. For a continuous function \(f: R_{+}^{*} \to C\) on the group \(R_{+}^{*}\) of positive real numbers, we define the Mellin transform to be the improper integral \[ L (f, s) = \int_ {0} ^ {\infty} (f (y) - f (\infty)) y ^ {s} \frac {d y}{y}, \] provided the limit \(f(\infty) = \lim_{y \to \infty} f(y)\) and the integral exist. The following theorem is of pivotal importance, also for later applications. We will often refer to it as the Mellin principle.

Formalized. Mathlib/Analysis/MellinTransform.lean::def mellin; Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean::structure WeakFEPair, WeakFEPair.hasMellin — Mathlib defines the Mellin transform on ℝ₊ and its functional-equation framework uses Mellin transforms of f-f₀, exactly Neukirch’s subtraction of the limiting constant term.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (1.4)

FC09-C07-U007 · Chapter VII, §1, source L17743 · in Mathlib

(1.4) Theorem. Let \(f, g: \mathbb{R}_+^* \to \mathbb{C}\) be continuous functions such that \[ f (y) = a _ {0} + O (e ^ {- c y ^ {\alpha}}), \quad g (y) = b _ {0} + O (e ^ {- c y ^ {\alpha}}), \] for \(y \to \infty\) , with positive constants \(c, \alpha\) . If these functions satisfy the equation \[ f \left(\frac {1}{y}\right) = C y ^ {k} g (y), \] for some real number \(k > 0\) and some complex number \(C \neq 0\) , then one has: (i) The integrals \(L(f, s)\) and \(L(g, s)\) converge absolutely and uniformly if \(s\) varies in an arbitrary compact domain contained in \(\{s \in \mathbb{C} \mid \operatorname{Re}(s) > k\}\) . They are therefore holomorphic functions on \(\{s \in \mathbb{C} \mid \operatorname{Re}(s) > k\}\) . They admit holomorphic continuations to \(\mathbb{C} \setminus \{0, k\}\) . (ii) They have simple poles at \(s = 0\) and \(s = k\) with residues \[ \operatorname{Res} _ {s = 0} L (f, s) = - a _ {0}, \quad \operatorname{Res} _ {s = k} L (f, s) = C b _ {0}, \quad r e s p. \] \[ \operatorname{Res} _ {s = 0} L (g, s) = - b _ {0}, \quad \operatorname{Res} _ {s = k} L (g, s) = C ^ {- 1} a _ {0}. \] (iii) They satisfy the functional equation \[ L (f, s) = C L (g, k - s). \] Remark 1: The symbol \(\varphi(y) = O(\psi(y))\) means, as usual, that one has \(\varphi(y) = c(y)\psi(y)\) , for some function \(c(y)\) which stays bounded under the limit in question, so in our case, as \(y \to \infty\) .

Formalized. Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean::structure WeakFEPair, differentiable_Λ₀, functional_equation, Λ_residue_k, Λ_residue_zero — WeakFEPair packages the kernel inversion and asymptotic constants; its Mellin construction proves meromorphic continuation, the two residues and the functional equation. Neukirch’s exponential-decay hypotheses imply the corresponding power-asymptotic bounds required by this interface.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (1.5)

FC09-C07-U008 · Chapter VII, §1, source L17827 · in Mathlib

(1.5) Proposition. The series \[ \theta (z) = \sum_ {n \in \mathbb {Z}} e ^ {\pi i n ^ {2} z} \] converges absolutely and uniformly in the domain \(\{z\in\mathbb{C}\mid\operatorname{Im}(z)\geq\delta\}\) , for every \(\delta>0\) . It therefore represents an analytic function on the upper half-plane \(H=\{z\in\mathbb{C}\mid\operatorname{Im}(z)>0\}\) , and satisfies the transformation formula \[ \theta (- 1 / z) = \sqrt {z / i} \theta (z). \]

Formalized. Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean::Complex.tsum_exp_neg_mul_int_sq; Mathlib/Analysis/Normed/Group/FunctionSeries.lean::tendstoUniformlyOn_tsum — With a=-i z, the Gaussian Poisson identity is exactly θ(-1/z)=√(z/i)θ(z). On Im(z)≥δ the terms are dominated by exp(-π n²δ), so the same uniform-series theorem gives the stated uniform convergence and holomorphy.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (1.6)

FC09-C07-U009 · Chapter VII, §1, source L17851 · in Mathlib

(1.6) Theorem. The completed zeta function \[ Z (s) = \pi^ {- s / 2} \Gamma (s / 2) \zeta (s) \] admits an analytic continuation to \(\mathbb{C} \setminus \{0,1\}\) , has simple poles at \(s = 0\) and \(s = 1\) with residues \(-1\) and \(1\) , respectively, and satisfies the functional equation \[ Z (s) = Z (1 - s). \]

Formalized. Mathlib/NumberTheory/LSeries/RiemannZeta.lean::differentiableAt_completedZeta, completedRiemannZeta_one_sub, completedRiemannZeta_residue_one — The completed zeta is differentiable off 0 and 1, symmetric under s↦1-s, and has residue +1 at 1; symmetry gives residue -1 at 0, exactly Proposition 1.8.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Corollary (1.7)

FC09-C07-U010 · Chapter VII, §1, source L17901 · in Mathlib

(1.7) Corollary. The Riemann zeta function \(\zeta(s)\) admits an analytic continuation to \(\mathbb{C} \setminus \{1\}\) , has a simple pole at \(s = 1\) with residue 1 and satisfies the functional equation \[ \zeta (1 - s) = 2 (2 \pi) ^ {- s} \Gamma (s) \cos \left(\frac {\pi s}{2}\right) \zeta (s). \]

Formalized. Mathlib/NumberTheory/LSeries/RiemannZeta.lean::analyticOn_riemannZeta, riemannZeta_residue_one, riemannZeta_one_sub — These declarations give the analytic continuation on ℂ{1}, residue one at s=1, and the exact Gamma-factor functional equation; the excluded Gamma poles are handled by analytic continuation as in Neukirch.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U011 · Chapter VII, §1, source L17949 · in Mathlib

These are explicit evaluations of the special values of the Riemann zeta function at the points \(s = 2k\) , \(k \in N\) . The phenomenon is explained via the functional equation by the fact that the values of the Riemann zeta function at the negative odd integers are given by Bernoulli numbers. These arise from the function \[ F (t) = \frac {t e ^ {t}}{e ^ {t} - 1} \] and are defined by the series expansion \[ F (t) = \sum_ {k = 0} ^ {\infty} B _ {k} \frac {t ^ {k}}{k !} \cdot \] Their relation to the zeta function gives them a special arithmetic significance. The first Bernoulli numbers are \[ B _ {0} = 1, B _ {1} = \frac {1}{2}, B _ {2} = \frac {1}{6}, B _ {3} = 0, B _ {4} = - \frac {1}{3 0}, B _ {5} = 0, B _ {6} = \frac {1}{4 2}. \] In general one has \(B_{2\nu+1}=0\) for \(\nu\geq1\) , because \(F(-t)=F(t)-t\) . In the classical literature, it is usually the function \(\frac{t}{e^{t}-1}\) , which serves for defining the Bernoulli numbers. As \(F(t)=\frac{t}{e^{t}-1}+t\) , this does not change anything except for \(B_{1}\) , where one finds \(-\frac{1}{2}\) instead of \(\frac{1}{2}\) . But the above definition is more natural and better suited for the further development of the theory. We now prove the remarkable theorem (1.8): for every integer \(k > 0\) one has \(\zeta(1-k) = -B_{k}/k\).

Formalized. Mathlib/NumberTheory/Bernoulli.lean::bernoulli'PowerSeries_mul_exp_sub_one, bernoulli'_zero, bernoulli'_one, bernoulli'_two, bernoulli'_three, bernoulli'_four, bernoulli'_eq_zero_of_odd — Mathlib’s bernoulli' is precisely Neukirch’s convention: its exponential generating function satisfies B’(t)(e^t-1)=t e^t, B’_1=+1/2, the displayed initial values agree, and all odd B’_n for n>1 vanish.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (1.8)

FC09-C07-U012 · Chapter VII, §1, source L17969 · in Mathlib

(1.8) Theorem. For every integer \(k > 0\) one has \[ \zeta (1 - k) = - \frac {B _ {k}}{k} \cdot \]

Formalized. Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean::riemannZeta_neg_nat_eq_bernoulli' — riemannZeta_neg_nat_eq_bernoulli' is exactly ζ(-k)=-B’_{k+1}/(k+1), equivalent after reindexing to Neukirch’s ζ(1-k)=-B’_k/k.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Lemma (1.9)

FC09-C07-U013 · Chapter VII, §1, source L17985 · not formalized

(1.9) Lemma. Let \(U\) be an open subset of \(\mathbb{C}\) that contains the path \(C_{\varepsilon, a}\) and also the interior of \(K_{\varepsilon}\) . Let \(G(z)\) be a holomorphic function on \(U \setminus \{0\}\) with a pole of order \(m\) at \(0\) , and let \(G(t)t^{ns-1} (n \in \mathbb{N})\) , for \(\operatorname{Re}(s) > \frac{m}{n}\) , be integrable on \((0, a)\) . Then one has \[ \int_ {C _ {\varepsilon , a}} G (z) z ^ {n s - 1} d z = (e ^ {2 \pi i n s} - 1) \int_ {0} ^ {a} G (t) t ^ {n s - 1} d t. \]

Not formalized. Pinned/current Mathlib contains substantial Riemann-zeta, Gamma, Bernoulli, theta and Dirichlet-L infrastructure, but this full source row requires an additional contour/special-value/zero statement not closed by the checked interfaces.

Corollary (1.10)

FC09-C07-U014 · Chapter VII, §1, source L18123 · in Mathlib

(1.10) Corollary. The values of \(\zeta(s)\) at the positive even integers \(s = 2k\) , \(k = 1, 2, 3, \ldots\) , are given by \[ \zeta (2 k) = (- 1) ^ {k - 1} \frac {(2 \pi) ^ {2 k}}{2 (2 k) !} B _ {2 k}. \]

Formalized. Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean::riemannZeta_two_mul_nat — This theorem is the exact Bernoulli/π formula for ζ(2k), with the standard Bernoulli convention identical to Neukirch’s in even degree.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U015 · Chapter VII, §1, source L18135 · not formalized

The image \(R_{2k}\) of a nonzero element in \(\tilde{K}_{4k-1}(\mathbb{Z}) \otimes_{\mathbb{Z}} \mathbb{Q}\) is called the 2k-th regulator. It is well-determined up to a rational factor, i.e., it is an element of \(R^{*}/Q^{*}\) , and one has \[ \zeta (2 k - 1) \equiv R _ {2 k} \bmod \mathbb {Q} ^ {*}. \] This discovery of the Swiss mathematician ARMAND BOREL has had a tremendous influence on further arithmetical research, and has opened up deep insights into the arithmetic nature of zeta functions and L-series of the most general kind. These insights are summarized within the comprehensive Beilinson conjecture (see [117]). In the meantime, the mathematicians SPENCER BLOCH and KAZUYA KATO have found a complete description of the special zeta values \(\zeta(2k-1)\) (i.e., not just a description mod \(Q^{*}\) ) via a new theory of the Tamagawa measure.

Definition / construction

FC09-C07-U016 · Chapter VII, §1, source L18143 · after FC09-C07-U001 · in Mathlib

The zeroes of the Riemann zeta function command special attention. Euler’s identity (1.1) shows that one has \(\zeta(s) \neq 0\) for \(\operatorname{Re}(s) > 1\) . The gamma function \(\Gamma(s)\) is nowhere 0 and has simple poles at \(s = 0, -1, -2, \ldots\) . The functional equation \(Z(s) = Z(1 - s)\) , i.e., \[ \pi^ {- s / 2} \Gamma (s / 2) \zeta (s) = \pi^ {(s - 1) / 2} \Gamma ((1 - s) / 2) \zeta (1 - s), \] therefore shows that the only zeroes of \(\zeta(s)\) in the domain \(\operatorname{Re}(s) < 0\) are the poles of \(\Gamma(s/2)\) , i.e., the arguments \(s = -2, -4, -6, \ldots\) . These are called the trivial zeroes of \(\zeta(s)\) . Other zeroes have to lie in the critical strip \(0 \leq \operatorname{Re}(s) \leq 1\) , since \(\zeta(s) \neq 0\) for \(\operatorname{Re}(s) > 1\) . They are the subject of the famous, still unproven Riemann Hypothesis: The non-trivial zeroes of \(\zeta(s)\) lie on the line \(\operatorname{Re}(s) = \frac{1}{2}\) .

Formalized. Mathlib/NumberTheory/LSeries/Nonvanishing.lean::riemannZeta_ne_zero_of_one_le_re; Mathlib/NumberTheory/LSeries/RiemannZeta.lean::riemannZeta_neg_two_mul_nat_add_one, RiemannHypothesis, riemannZeta_one_sub — Pinned Mathlib proves nonvanishing for Re(s)≥1, all negative-even zeros, and packages RH. Combining the functional equation with Gamma nonvanishing gives that the negative-even zeros are the only zeros for Re(s)<0, hence the remaining zeros lie in the critical strip.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U017 · Chapter VII, §2, source L18240 · in Mathlib

The most immediate relatives of the Riemann zeta function are the Dirichlet L-series. They are defined as follows. Let m be a natural number. A Dirichlet character mod m is by definition a character \[ \chi : (\mathbb {Z} / m \mathbb {Z}) ^ {*} \longrightarrow S ^ {1} = \left\{z \in \mathbb {C} \mid | z | = 1 \right\}. \] It is called primitive if it does not arise as the composite \[ (\mathbb {Z} / m \mathbb {Z}) ^ {*} \longrightarrow (\mathbb {Z} / m ^ {\prime} \mathbb {Z}) ^ {*} \stackrel {\chi^ {\prime}} {\longrightarrow} S ^ {1} \] of a Dirichlet character \(\chi'\) mod \(m'\) for any proper divisor \(m'|m\) . In the general case, the gcd of all such divisors is called the conductor \(f\) of \(\chi\) . So \(\chi\) is always induced from a primitive character \(\chi'\) mod \(f\) . Given \(\chi\) , we define the multiplicative function \(\chi: \mathbb{Z} \to \mathbb{C}\) by \[ \chi (n) = \left\{ \begin{array}{l l} \chi (n \bmod m) & \text { for } (n, m) = 1, \\ 0 & \text { for } (n, m) \neq 1. \end{array} \right. \] The trivial character \(\chi^{0} \mod m\) , \(\chi^{0}(n)=1\) for \((n,m)=1\) , \(\chi^{0}(n)=0\) for \((n,m)\neq1\) , plays a special role. When read mod 1, we denote it by \(\chi=1\) . It is also called the principal character. Considering it in the theory to be developed now has the effect of subsuming here everything we have done in the last section. For a Dirichlet character \(\chi\) , we form the Dirichlet L-series \[ L(\chi,s) = \sum_{n=1}^{\infty} \frac{\chi(n)}{n^{s}}, \] for a complex variable \(s\) with \(\operatorname{Re}(s) > 1\).

Formalized. Mathlib/NumberTheory/DirichletCharacter/Basic.lean::DirichletCharacter, FactorsThrough, def conductor, def IsPrimitive, def primitiveCharacter, changeLevel_primitiveCharacter — Mathlib’s conductor is the least modulus through which the character factors; IsPrimitive and primitiveCharacter package exactly Neukirch’s primitive/induced character reduction.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.1)

FC09-C07-U018 · Chapter VII, §2, source L18268 · in Mathlib

(2.1) Proposition. The series \(L(\chi, s)\) converges absolutely and uniformly in the domain \(\operatorname{Re}(s) \geq 1 + \delta\) , for any \(\delta > 0\) . It therefore represents an analytic function on the half-plane \(\operatorname{Re}(s) > 1\) . We have Euler’s identity \[ L (\chi , s) = \prod_ {p} {\frac {1}{1 - \chi (p) p ^ {- s}}}. \]

Formalized. Mathlib/NumberTheory/LSeries/Dirichlet.lean::LSeriesSummable_of_one_lt_re; Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean::DirichletCharacter.LSeries_eulerProduct; Mathlib/Analysis/Normed/Group/FunctionSeries.lean::tendstoUniformlyOn_tsum — The Dirichlet-character L-series is absolutely summable for Re(s)>1 and has the expected Euler product. Since |χ(n)|≤1, zeta’s n^-(1+δ) majorant gives uniform convergence on every Re(s)≥1+δ and hence holomorphy.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U019 · Chapter VII, §2, source L18278 · not formalized

The proof again hinges on an integral representation of the function \(L(\chi, s)\) which has the effect of realizing it as the Mellin transform of a theta series. We do, however, have to distinguish now between even and odd Dirichlet characters \(\chi \mod m\) . This phenomenon will become increasingly important when we generalize further. We define the exponent \(p \in \{0, 1\}\) of \(\chi\) by \[ \chi (- 1) = (- 1) ^ {p} \chi (1). \] Then the rule \[ \chi ((n)) = \chi (n) \left(\frac {n}{| n |}\right) ^ {p} \] defines a multiplicative function on the semigroup of all ideals \((n)\) which are relatively prime to m. This function is called a Größencharakter mod m. These Größencharaktere are capable of substantial generalization and will play the leading part when we consider higher algebraic number fields (see §7).

Not formalized. Pinned/current Mathlib has Dirichlet characters, primitive conductors, Gauss sums and completed Dirichlet L-functions, but this row requires a Größencharacter, generalized Bernoulli value formula, theta transform, or primitive Gauss-sum modulus statement not exported as a complete compatible owner.

Definition / construction

FC09-C07-U020 · Chapter VII, §2, source L18340 · after FC09-C07-U018 · in Mathlib

We view the factor \[ L _ {\infty} (\chi , s) = \left(\frac {m}{\pi}\right) ^ {s / 2} \Gamma (\chi , s) \] in (*) as the “Euler factor” at the infinite prime. It joins with the Euler factors \(L_{p}(s)=1/(1-\chi(p)p^{-s})\) of the product representation (2.1) of \(L(\chi,s)\) to define the completed L-series of the character \(\chi\) : \[ \Lambda (\chi , s) = L _ {\infty} (\chi , s) L (\chi , s), \quad \operatorname{Re} (s) > 1. \]

Formalized. Mathlib/NumberTheory/LSeries/DirichletContinuation.lean::def gammaFactor, Even.gammaFactor_def, Odd.gammaFactor_def, def completedLFunction, LFunction_eq_completed_div_gammaFactor — Mathlib splits the Gamma factor by parity χ(-1)=±1 and defines the completed L-function. Its normalization differs by the harmless explicit N^{s/2} scalar used by Neukirch, so the displayed source object is recovered by renormalization.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.2)

FC09-C07-U021 · Chapter VII, §2, source L18354 · not formalized

(2.2) Proposition. The function \(\Lambda(\chi, s)\) admits the integral representation \[ \Lambda (\chi , s) = \frac {c (\chi)}{2} \int_ {0} ^ {\infty} \left(\theta (\chi , i y) - \chi (0)\right) y ^ {(s + p) / 2} \frac {d y}{y}, \] where \(c(\chi) = (\frac{\pi}{m})^{p / 2}\) .

Proposition (2.3)

FC09-C07-U022 · Chapter VII, §2, source L18366 · not formalized

(2.3) Proposition. Let \(a, b, \mu\) be real numbers, \(\mu > 0\) . Then the series \[ \theta_ {\mu} (a, b, z) = \sum_ {g \in \mu \mathbb {Z}} e ^ {\pi i (a + g) ^ {2} z + 2 \pi i b g} \] converges absolutely and uniformly in the domain \(\operatorname{Im}(z) \geq \delta\) , for every \(\delta > 0\) , and for \(z \in \mathbb{H}\) , one has the transformation formula \[ \theta_ {\mu} (a, b, - 1 / z) = e ^ {- 2 \pi i a b} \frac {\sqrt {z / i}}{\mu} \theta_ {1 / \mu} (- b, a, z). \]

Corollary (2.4)

FC09-C07-U023 · Chapter VII, §2, source L18398 · not formalized

(2.4) Corollary. For \(a, b, \mu \in \mathbb{R}\) , \(\mu > 0\) , one has the transformation formula \[ \theta_ {\mu} ^ {p} (a, b, - 1 / z) = \left[ i ^ {p} e ^ {2 \pi i a b} \mu \right] ^ {- 1} (z / i) ^ {p + \frac {1}{2}} \theta_ {1 / \mu} ^ {p} (- b, a, z). \]

Definition / construction

FC09-C07-U024 · Chapter VII, §2, source L18404 · not formalized

This corollary gives us the required transformation formula for the theta series \(\theta (\chi ,a)\) , if we introduce the Gauss sums which are defined as follows.

Definition (2.5)

FC09-C07-U025 · Chapter VII, §2, source L18406 · in Mathlib

(2.5) Definition. For \(n \in Z\) , the Gauss sum \(\tau(\chi, n)\) associated to the Dirichlet character \(\chi \mod m\) is defined to be the complex number \[ \tau (\chi , n) = \sum_ {\nu = 0} ^ {m - 1} \chi (\nu) e ^ {2 \pi i \nu n / m}. \] For \(n = 1\) , we write \(\tau(\chi) = \tau(\chi, 1)\) .

Formalized. Mathlib/NumberTheory/GaussSum.lean::def gaussSum; Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean::def stdAddChar; Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean::gaussSum_mulShift_of_isPrimitive — The general Gauss sum applied to a Dirichlet multiplicative character and the standard additive character of Z/NZ is Neukirch’s τ(χ,n); mulShift is the n-shift of the additive character.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.6)

FC09-C07-U026 · Chapter VII, §2, source L18414 · not formalized

(2.6) Proposition. For a primitive Dirichlet character \(\chi \bmod m\) , one has \[ \tau (\chi , n) = \overline {{{{\chi}}}} (n) \tau (\chi) \quad a n d \quad | \tau (\chi) | = \sqrt {m}. \]

Proposition (2.7)

FC09-C07-U027 · Chapter VII, §2, source L18438 · not formalized

(2.7) Proposition. If \(\chi\) is a primitive Dirichlet character mod \(m\) , then we have the transformation formula \[ \theta (\chi , - 1 / z) = \frac {\tau (\chi)}{i ^ {p} \sqrt {m}} (z / i) ^ {p + \frac {1}{2}} \theta (\overline {{\chi}}, z), \] where \(\overline{\chi}\) is the complex conjugate character to \(\chi\) , i.e., its inverse.

Theorem (2.8)

FC09-C07-U028 · Chapter VII, §2, source L18484 · not formalized

(2.8) Theorem. If \(\chi\) is a nontrivial primitive Dirichlet character, then the completed L-series \(\Lambda(\chi,s)\) admits an analytic continuation to the whole complex plane C and satisfies the functional equation \[ \Lambda (\chi , s) = W (\chi) \Lambda (\overline {{{{\chi}}}}, 1 - s) \] with the factor \(W(\chi) = \frac{\tau(\chi)}{i^p\sqrt{m}}\) . This factor has absolute value 1.

Definition / construction

FC09-C07-U029 · Chapter VII, §2, source L18524 · not formalized

For a nontrivial primitive Dirichlet character \(\chi \bmod m\), the generalized Bernoulli numbers \(B_{k,\chi}\) are defined by \[ F_{\chi}(t) = \sum_{a=1}^{m} \chi(a)\frac{te^{at}}{e^{mt}-1} = \sum_{k=0}^{\infty} B_{k,\chi}\frac{t^{k}}{k!}, \] algebraic numbers lying in \(\mathbb{Q}(\chi)\). Since \(F_{\chi}(-t) = \chi(-1)F_{\chi}(t)\), one finds \((-1)^{k}B_{k,\chi} = \chi(-1)B_{k,\chi}\), so that \(B_{k,\chi} = 0\) whenever \((-1)^{k} \neq \chi(-1)\).

Convention / notation

FC09-C07-U030 · Chapter VII, §2, source L18542 · in Mathlib

\(p \in \{0,1\}\) is defined by \(\chi(-1) = (-1)^p \chi(1)\) .

Formalized. Mathlib/NumberTheory/DirichletCharacter/Basic.lean::def Odd, def Even, even_or_odd, Odd.toUnitHom_eval_neg_one, Even.toUnitHom_eval_neg_one — This is exactly the source convention p∈{0,1} determined by χ(-1)=(-1)^p.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (2.9)

FC09-C07-U031 · Chapter VII, §2, source L18544 · not formalized

(2.9) Theorem. For any integer \(k \geq 1\) , one has \[ L (\chi , 1 - k) = - \frac {B _ {k , \chi}}{k}. \]

Corollary (2.10)

FC09-C07-U032 · Chapter VII, §2, source L18596 · not formalized

(2.10) Corollary. For \(k \equiv p \mod 2\) , \(k \geq 1\) , one has \[ L (\chi , k) = (- 1) ^ {1 + (k - p) / 2} \frac {\tau (\chi)}{2 i ^ {p}} \Bigl (\frac {2 \pi}{m} \Bigr) ^ {k} \frac {B _ {k , \overline {{\chi}}}}{k !}. \]

Convention / notation

FC09-C07-U033 · Chapter VII, §3, source L18634 · not formalized

The familiar objects \(\mathbb{C}\) , \(\mathbb{R}\) , \(\mathbb{R}_{+}^{*}\) , \(\mathbb{H}\) , \(|\cdot|\) , log, find their higher dimensional analogues as follows. Let \(X\) be a finite \(G(\mathbb{C}|\mathbb{R})\) -set, i.e., a finite set with an involution \(\tau \mapsto \overline{\tau}\) ( \(\tau \in X\) ), and let \(n = \# X\) . We consider the \(n\) -dimensional \(\mathbb{C}\) -algebra \[ \mathbf {C} = \prod_ {\tau \in X} \mathbb {C} \] of all tuples \(z = (z_{\tau})_{\tau \in X}\) , \(z_{\tau} \in C\) , with componentwise addition and multiplication. If \(z = (z_{\tau}) \in \mathbf{C}\) , then the element \(\bar{z} \in C\) is defined to have the following components: \[ (\bar {z}) _ {\tau} = \bar {z} _ {\overline {{\tau}}}. \] We call the involution \(z \mapsto \bar{z}\) the conjugation on C. In addition, we have the involutions \(z \mapsto z^{*}\) and \(z \mapsto ^{*}z\) given by \[ z _ {\tau} ^ {*} = z _ {\overline {{{\tau}}}}, \quad \text {resp.} \quad {} ^ {*} z _ {\tau} = \bar {z} _ {\tau}. \] One clearly has \(\bar{z} = {}^{*}z^{*}\) . The set \[ \mathbf {R} = \left[ \prod_ {\tau} \mathbb {C} \right] ^ {+} = \left\{z \in \mathbf {C} \mid z = \bar {z} \right\} \] forms an \(n\) -dimensional commutative \(\mathbb{R}\) -algebra, and \(\mathbf{C} = \mathbf{R} \otimes_{\mathbb{R}} \mathbb{C}\) .

Not formalized. Mathlib and the checked AINTLIB development provide Schwartz Fourier transforms, Gaussian transforms, and lattice Poisson summation; this row additionally requires Neukirch’s shifted/polynomial multivariable theta package or its full transformation law, which is not packaged by the checked interfaces.

Convention / notation

FC09-C07-U034 · Chapter VII, §3, source L18662 · not formalized

For the additive, resp. multiplicative, group C, resp. \(C^{*}\) , we have the homomorphism \[ \begin{array}{l} T r: \mathbf {C} \to \mathbb {C}, \quad T r (z) = \sum_ {\tau} z _ {\tau}, \quad \text {resp.} \\ N: \mathbf {C} ^ {*} \to \mathbb {C} ^ {*}, N (z) = \prod_ {\tau} z _ {\tau}. \end{array} \] Here \(Tr(z)\) , resp. \(N(z)\) , denotes the trace, resp. the determinant, of the endomorphism \(C \rightarrow C\) , \(x \mapsto zx\) . Furthermore we have on C the hermitian scalar product \[ \langle x, y \rangle = \sum_ {\tau} x _ {\tau} \bar {y} _ {\tau} = T r (x ^ {*} y). \] It is invariant under conjugation, \(\overline{\langle x,y\rangle}=\langle\bar{x},\bar{y}\rangle\) , and restricting it yields a scalar product \(\langle,\rangle\) , i.e., a euclidean metric, on the R-vector space R. If \(z\in C\) , then \(^{*}z\) is the adjoint element with respect to \(\langle,\rangle\) , i.e., \[ \langle x z, y \rangle = \langle x, ^ {*} z y \rangle . \]

Convention / notation

FC09-C07-U035 · Chapter VII, §3, source L18680 · not formalized

In \(\mathbf{R}\) , we consider the subspace \[ \mathbf {R} _ {\pm} = \left\{x \in \mathbf {R} \mid x = x ^ {*} \right\} = \left[ \prod_ {\tau} \mathbb {R} \right] ^ {+}. \] Thus we find for the components of \(x = (x_{\tau}) \in \mathbf{R}_{\pm}\) that \(x_{\overline{\tau}} = x_{\tau} \in R\) . If \(\delta \in R\) , we simply write \(x > \delta\) to signify that \(x_{\tau} > \delta\) for all \(\tau\) . The multiplicative group \[ \mathbf {R} _ {+} ^ {*} = \left\{x \in \mathbf {R} _ {\pm} \mid x > 0 \right\} = \left[ \prod_ {\tau} \mathbb {R} _ {+} ^ {*} \right] ^ {+} \] will play a particularly important part. It consists of the tuples \(x = (x_{\tau})\) of positive real numbers \(x_{\tau}\) such that \(x_{\overline{\tau}} = x_{\tau}\) , and it occurs in the two homomorphisms \[ | \quad |: \mathbf {R} ^ {*} \longrightarrow \mathbf {R} _ {+} ^ {*}, \quad x = (x _ {\tau}) \longmapsto | x | = (| x _ {\tau} |), \] \[ \log : \mathbf {R} _ {+} ^ {*} \stackrel {{\sim}} {{\longrightarrow}} \mathbf {R} _ {\pm}, \quad x = (x _ {\tau}) \longmapsto \log x = (\log x _ {\tau}). \]

Definition / construction

FC09-C07-U036 · Chapter VII, §3, source L18702 · not formalized

We finally define the upper half-space associated to the \(G(\mathbb{C}|\mathbb{R})\) -set X by \[ \mathbf {H} = \mathbf {R} _ {\pm} + i \mathbf {R} _ {+} ^ {*}. \] Putting \(\operatorname{Re}(z) = \frac{1}{2} (z + \bar{z})\) , \(\operatorname{Im}(z) = \frac{1}{2i} (z - \bar{z})\) , we may also write \[ \mathbf {H} = \left\{z \in \mathbf {C} \mid z = z ^ {*}, \operatorname{Im} (z) > 0 \right\}. \]

Convention / notation

FC09-C07-U037 · Chapter VII, §3, source L18716 · not formalized

For two tuples \(z = (z_{\tau})\) , \(p = (p_{\tau}) \in \mathbf{C}\) , the power \[ z ^ {p} = (z _ {\tau} ^ {p _ {\tau}}) \in \mathbf {C} \] is well-defined by \[ z _ {\tau} ^ {p _ {\tau}} = e ^ {p _ {\tau} \log z _ {\tau}}, \] if we agree to take the principal branch of the logarithm and assume that the \(z_{\tau}\) move only in the plane cut along the negative real axis. The table \[ \mathbb {H} \subseteq \mathbb {C} \supseteq \mathbb {R} = \mathbb {R} \supseteq \mathbb {R} _ {+} ^ {*}, | |: \mathbb {R} ^ {*} \rightarrow \mathbb {R} _ {+} ^ {*}, \log : \mathbb {R} _ {+} ^ {*} \stackrel {{\sim}} {{\longrightarrow}} \mathbb {R}, \] \[ \mathbf {H} \subseteq \mathbf {C} \supseteq \mathbf {R} \supseteq \mathbf {R} _ {\pm} \supseteq \mathbf {R} _ {+} ^ {*}, \quad | |: \mathbf {R} ^ {*} \rightarrow \mathbf {R} _ {+} ^ {*}, \quad \log : \mathbf {R} _ {+} ^ {*} \stackrel {{\sim}} {{\longrightarrow}} \mathbf {R} _ {\pm}, \] shows the analogy of the notions introduced with the familiar ones in the case n = 1. We recommend that the reader memorize them well, for they will be used constantly in what follows without special cross-reference. This also includes the notation \[ \bar {z}, z ^ {*}, ^ {*} z, T r, N, \langle , \rangle , x > \delta , z ^ {p}. \]

Definition / construction

FC09-C07-U038 · Chapter VII, §3, source L18744 · in Mathlib

The functional equations we are envisaging originate in a general formula from functional analysis, the Poisson summation formula. It will be proved first. A Schwartz function (or rapidly decreasing function) on a euclidean vector space R is by definition a \(C^{\infty}\) -function \(f: R \to C\) which tends to zero as \(x \to \infty\) , even if multiplied by an arbitrary power \(\|x\|^{m}, m \geq 0\) , and which shares this behaviour with all its derivatives. For every Schwartz function f, one forms the Fourier transform \[ \widehat {f} (y) = \int_ {\mathbf {R}} f (x) e ^ {- 2 \pi i \langle x, y \rangle} d x, \] where dx is the Haar measure on R associated to \(\langle\ ,\ \rangle\) which ascribes the volume 1 to the cube spanned by an orthonormal basis, i.e., it is the Haar measure which is selfdual with respect to \(\langle\ ,\ \rangle\) . The improper integral converges absolutely and uniformly and gives again a Schwartz function \(\widehat{f}\) . This is easily proved by elementary analytical techniques; we refer also to [98], chap. XIV. The prototype of a Schwartz function is the function \[ h (x) = e ^ {- \pi \langle x, x \rangle}. \]

Formalized. Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean::SchwartzMap, norm_pow_mul_le_seminorm; Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean::fourierTransformCLM, fourier_coe — Mathlib’s Schwartz space is defined by rapid decay of all derivatives; its Fourier transform is a continuous linear self-map/equivalence of Schwartz space with the standard integral normalization, exactly the structure introduced in U038.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (3.1)

FC09-C07-U039 · Chapter VII, §3, source L18758 · in another Lean project

(3.1) Proposition. (i) The function \(h(x) = e^{-\pi \langle x, x \rangle}\) is its own Fourier transform. (ii) If \(f\) is an arbitrary Schwartz function and \(A\) is a linear transformation of \(\mathbf{R}\) , then the function \(f_{A}(x) = f(Ax)\) has Fourier transform \[ \widehat {f} _ {A} (y) = \frac {1}{| \det A |} \widehat {f} (^ {t} A ^ {- 1} y), \] where \(^{t}A\) is the adjoint transformation of A.

Formalized. CBirkbeck/AINTLIB@160e446617a2168c34c95bbe7a76c4105b392434/projects/DedekindResidue/DedekindResidue/CompletedZeta/ThetaLattice.lean::fourier_gaussianCM; CBirkbeck/AINTLIB@160e446617a2168c34c95bbe7a76c4105b392434/projects/DedekindResidue/DedekindResidue/CompletedZeta/PoissonLattice.lean::fourier_comp_linearEquiv — AINTLIB proves the n-dimensional Gaussian transform with the exact t^{-n/2} scaling and the full GL change-of-variables formula |det T|⁻¹ · Fg((T⁻¹)^*w). Setting t=1 gives Gaussian self-duality, so both parts of Proposition 3.1 are source-complete.

Searched: R=160e446617a2168c34c95bbe7a76c4105b392434 (Mathlib pin e4b72ca0d01c5f45c485814ec129debbc4f64634, Apache-2.0); P=db584cd6d46c92f209a44c0f1c829460d327499d

Poisson Summation Formula (3.2)

FC09-C07-U040 · Chapter VII, §3, source L18790 · in another Lean project

(3.2) Poisson Summation Formula. Let \(\Gamma\) be a complete lattice in \(\mathbf{R}\) and let \[ \Gamma^ {\prime} = \left\{g ^ {\prime} \in \mathbf {R} \mid \langle g, g ^ {\prime} \rangle \in \mathbb {Z} \text { for all } g \in \Gamma \right\} \] be the lattice dual to \(\Gamma\) . Then for any Schwartz function f, one has: \[ \sum_ {g \in \Gamma} f (g) = \frac {1}{\operatorname{vol} (\Gamma)} \sum_ {g ^ {\prime} \in \Gamma^ {\prime}} \widehat {f} (g ^ {\prime}), \] where \(\operatorname{vol}(\Gamma)\) is the volume of a fundamental mesh of \(\Gamma\) .

Formalized. CBirkbeck/AINTLIB@160e446617a2168c34c95bbe7a76c4105b392434/projects/DedekindResidue/DedekindResidue/CompletedZeta/DualLattice.lean::def dualZLattice, covolume_dualZLattice_mul; CBirkbeck/AINTLIB@160e446617a2168c34c95bbe7a76c4105b392434/projects/DedekindResidue/DedekindResidue/CompletedZeta/PoissonLattice.lean::tsum_eq_tsum_fourier_zlattice; Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean::norm_pow_mul_le_seminorm; Mathlib/Algebra/Module/ZLattice/Summable.lean::summable_norm_rpow; Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean::fourierTransformCLM — The external theorem is exactly the lattice/dual/covolume Poisson formula under the two natural summability hypotheses. For a Schwartz function, pinned rapid-decay seminorm bounds plus ZLattice.summable_norm_rpow discharge both lattice-sum hypotheses (also for its Fourier transform), yielding Neukirch’s unrestricted Schwartz statement.

Searched: R=160e446617a2168c34c95bbe7a76c4105b392434 (Mathlib pin e4b72ca0d01c5f45c485814ec129debbc4f64634, Apache-2.0); P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U041 · Chapter VII, §3, source L18864 · not formalized

We apply the Poisson summation formula to the functions \[ f _ {p} (a, b, x) = N \left((x + a) ^ {p}\right) e ^ {- \pi \langle a + x, a + x \rangle + 2 \pi i \langle b, x \rangle} \] with the parameters \(a, b \in R\) and a tuple \(p = (p_{\tau})\) of nonnegative integers, such that \(p_{\tau} \in \{0, 1\}\) if \(\tau = \overline{\tau}\) , and \(p_{\tau} p_{\overline{\tau}} = 0\) if \(\tau \neq \overline{\tau}\) . Such an element \(p \in \prod_{\tau} Z\) will henceforth be called admissible.

Proposition (3.3)

FC09-C07-U042 · Chapter VII, §3, source L18872 · not formalized

(3.3) Proposition. The function \(f(x) = f_{p}(a, b, x)\) is a Schwartz function on \(\mathbf{R}\) . Its Fourier transform is \[ \widehat {f} (y) = \left[ i ^ {T r (p)} e ^ {2 \pi i \langle a, b \rangle} \right] ^ {- 1} f _ {p} (- b, a, y). \]

Definition (3.4)

FC09-C07-U043 · Chapter VII, §3, source L18958 · not formalized

(3.4) Definition. For every complete lattice \(\Gamma\) of \(\mathbf{R}\) , we define the theta series \[ \theta_ {\Gamma} (z) = \sum_ {g \in \Gamma} e ^ {\pi i \langle g z, g \rangle}, \quad z \in \mathbf {H}. \] More generally, for \(a, b \in \mathbf{R}\) and any admissible \(p \in \prod_{\tau} \mathbb{Z}\) , we put \[ \theta_ {\Gamma} ^ {p} (a, b, z) = \sum_ {g \in \Gamma} N \big ((a + g) ^ {p} \big) e ^ {\pi i \langle (a + g) z, a + g \rangle + 2 \pi i \langle b, g \rangle}. \]

Proposition (3.5)

FC09-C07-U044 · Chapter VII, §3, source L18970 · not formalized

(3.5) Proposition. The series \(\theta_{\Gamma}^{p}(a,b,z)\) converges absolutely and uniformly on every compact subset of \(R \times R \times H\) .

Theta Transformation Formula (3.6)

FC09-C07-U045 · Chapter VII, §3, source L19014 · not formalized

(3.6) Theta Transformation Formula. One has \[ \theta_ {\Gamma} ^ {p} (a, b, - 1 / z) = \left[ i ^ {T r (p)} e ^ {2 \pi i \langle a, b \rangle} \mathrm{vol} (\Gamma) \right] ^ {- 1} N \Big ((z / i) ^ {p + \frac {1}{2}} \Big) \theta_ {\Gamma^ {\prime}} ^ {p} (- b, a, z). \] In particular, one has for the function \(\theta_{\Gamma}(z) = \theta_{\Gamma}^{0}(0,0,z)\) : \[ \theta_ {\Gamma} (- 1 / z) = \frac {\sqrt {N (z / i)}}{\operatorname{vol} (\Gamma)} \theta_ {\Gamma^ {\prime}} (z). \]

Definition / construction

FC09-C07-U046 · Chapter VII, §4, source L19108 · not formalized

In order to generalize this process, we now introduce a higher-dimensional gamma function for every finite \(G(\mathbb{C}|\mathbb{R})\) -set X, building upon the notation of the last section. First we fix a Haar measure on the multiplicative group \(R_{+}^{*}\) : Let \(\mathfrak{p} = \{\tau, \overline{\tau}\}\) be the conjugation classes in \(X\) . We call \(\mathfrak{p}\) real or complex, depending whether \(\# \mathfrak{p} = 1\) or \(\# \mathfrak{p} = 2\) . We then have \[ \mathbf {R} _ {+} ^ {*} = \prod_ {\mathfrak {p}} \mathbf {R} _ {+ \mathfrak {p}} ^ {*}, \] where \[ \mathbf {R} _ {+ \mathfrak {p}} ^ {*} = \mathbb {R} _ {+} ^ {*}, \quad \text { resp. } \quad \mathbf {R} _ {+ \mathfrak {p}} ^ {*} = \left[ \mathbb {R} _ {+} ^ {*} \times \mathbb {R} _ {+} ^ {*} \right] ^ {+} = \left\{(y, y) \mid y \in \mathbb {R} _ {+} ^ {*} \right\}. \] We define isomorphisms \[ \mathbf {R} _ {+ \mathfrak {p}} ^ {*} \stackrel {\sim} {\longrightarrow} \mathbb {R} _ {+} ^ {*} \] by \(y \mapsto y\) , resp. \((y, y) \mapsto y^2\) , and obtain an isomorphism \[ \varphi : \mathbf {R} _ {+} ^ {*} \stackrel {{\sim}} {{\longrightarrow}} \prod_ {\mathfrak {p}} \mathbb {R} _ {+} ^ {*}. \] We now denote by \(\frac{dy}{y}\) the Haar measure on \(R_{+}^{*}\) which corresponds to the product measure \[ \prod_ {\mathfrak {p}} \frac {d t}{t}, \] where \(\frac{dt}{t}\) is the usual Haar measure on \(\mathbb{R}_+^*\) . The Haar measure thus defined is called the canonical measure on \(\mathbf{R}_+^*\) . Under the logarithm \[ \log : \mathbf {R} _ {+} ^ {*} \stackrel {{\sim}} {{\longrightarrow}} \mathbf {R} _ {\pm}, \] it is mapped to the Haar measure dx on \(R_{\pm}\) which under the isomorphism \[ \mathbf {R} _ {\pm} = \prod_ {\mathfrak {p}} \mathbf {R} _ {\pm \mathfrak {p}} \xrightarrow {\varphi} \prod_ {\mathfrak {p}} \mathbb {R}, \] \(x_{\mathfrak{p}} \mapsto x_{\mathfrak{p}}\) , resp. \((x_{\mathfrak{p}}, x_{\mathfrak{p}}) \mapsto 2x_{\mathfrak{p}}\) , corresponds to the Lebesgue measure on \(\prod_{\mathfrak{p}} \mathbb{R}\) .

Not formalized. The checked analytic libraries do not package Neukirch’s G(C/R)-set gamma/L-factor formalism with all norm and determinant identities in this source unit.

Definition (4.1)

FC09-C07-U047 · Chapter VII, §4, source L19154 · not formalized

(4.1) Definition. For \(\mathbf{s} = (s_{\tau}) \in \mathbf{C}\) such that \(\operatorname{Re}(s_{\tau}) > 0\) , we define the gamma function associated to the \(G(\mathbb{C}|\mathbb{R})\) -set X by \[ \Gamma_ {X} (\mathbf {s}) = \int_ {\mathbf {R} _ {+} ^ {*}} N (e ^ {- y} y ^ {\mathbf {s}}) \frac {d y}{y}. \]

Not formalized. The checked analytic libraries do not package Neukirch’s G(C/R)-set gamma/L-factor formalism with all norm and determinant identities in this source unit.

Proposition (4.2)

FC09-C07-U048 · Chapter VII, §4, source L19162 · not formalized

(4.2) Proposition. Decomposing the \(G(\mathbb{C}|\mathbb{R})\) -set \(X\) into its conjugation classes \(\mathfrak{p}\) , one has \[ \Gamma_ {X} (\mathbf {s}) = \prod_ {\mathfrak {p}} \Gamma_ {\mathfrak {p}} (\mathbf {s} _ {\mathfrak {p}}), \] where \(\mathbf{s}_{\mathfrak{p}} = s_{\tau}\) for \(\mathfrak{p} = \{\tau\}\) , resp. \(\mathbf{s}_{\mathfrak{p}} = (s_{\tau}, s_{\overline{\tau}})\) for \(\mathfrak{p} = \{\tau, \overline{\tau}\}\) , \(\tau \neq \overline{\tau}\) . The factors are given explicitly by \[ \Gamma_ {\mathfrak {p}} (\mathbf {s} _ {\mathfrak {p}}) = \left\{ \begin{array}{l l} \Gamma (\mathbf {s} _ {\mathfrak {p}}), & \text {if \mathfrak {p} real}, \\ 2 ^ {1 - T r (\mathbf {s} _ {\mathfrak {p}})} \Gamma (T r (\mathbf {s} _ {\mathfrak {p}})), & \text {if \mathfrak {p} complex}, \end{array} \right. \] where \(Tr(\mathbf{s}_{\mathfrak{p}}) = s_{\tau} + s_{\overline{\tau}}\) .

Not formalized. The checked analytic libraries do not package Neukirch’s G(C/R)-set gamma/L-factor formalism with all norm and determinant identities in this source unit.

Definition / construction

FC09-C07-U049 · Chapter VII, §4, source L19202 · after FC09-C07-U048 · not formalized

We call the function \[ L _ {X} (\mathbf {s}) = N (\pi^ {- \mathbf {s} / 2}) \Gamma_ {X} (\mathbf {s} / 2) \] the \(L\) -function of the \(G(\mathbb{C}|\mathbb{R})\) -set \(X\) . Decomposing \(X\) into the conjugation classes \(\mathfrak{p}\) , yields \[ L _ {X} (\mathbf {s}) = \prod_ {\mathfrak {p}} L _ {\mathfrak {p}} (\mathbf {s} _ {\mathfrak {p}}), \] where as before we write \(\mathbf{s}_{\mathfrak{p}} = s_{\tau}\) for \(\mathfrak{p} = \{\tau\}\) and \(\mathbf{s}_{\mathfrak{p}} = (s_{\tau}, s_{\overline{\tau}})\) for \(\mathfrak{p} = \{\tau, \overline{\tau}\}\) , \(\tau \neq \overline{\tau}\) . The factors \(L_{\mathfrak{p}}(\mathbf{s}_{\mathfrak{p}})\) are given explicitly, by (4.2), as \[ L _ {\mathfrak {p}} (\mathbf {s} _ {\mathfrak {p}}) = \left\{ \begin{array}{l l} \pi^ {- \mathbf {s} _ {\mathfrak {p}} / 2} \Gamma (\mathbf {s} _ {\mathfrak {p}} / 2), & \text {if \mathfrak {p} real}, \\ 2 (2 \pi) ^ {- T r (\mathbf {s} _ {\mathfrak {p}}) / 2} \Gamma (T r (\mathbf {s} _ {\mathfrak {p}}) / 2), & \text {if \mathfrak {p} complex}. \end{array} \right. \] For a single complex variable \(s \in \mathbb{C}\) , we put \[ \Gamma_ {X} (s) = \Gamma_ {X} (s {\bf 1}), \] where \(\mathbf{1} = (1, \ldots, 1)\) is the unit element of \(\mathbf{C}\) . Denoting \(r_1\) , resp. \(r_2\) , the number of real, resp. complex, conjugation classes of \(X\) , we find \[ \Gamma_ {X} (s) = 2 ^ {(1 - 2 s) r _ {2}} \Gamma (s) ^ {r _ {1}} \Gamma (2 s) ^ {r _ {2}}. \] In the same way we put \[ L _ {X} (s) = L _ {X} (s \mathbf {1}) = \pi^ {- n s / 2} \Gamma_ {X} (s / 2), \quad n = \# X, \] and in particular \[ L _ {\mathbb {R}} (s) = L _ {X} (s) = \pi^ {- s / 2} \Gamma (s / 2), \quad \mathrm{if} \quad X = \{\tau \}, \] \[ L _ {\mathbb {C}} (s) = L _ {X} (s) = 2 (2 \pi) ^ {- s} \Gamma (s), \quad \text { if } \quad X = \{\tau , \overline {{\tau}} \}, \tau \neq \overline {{\tau}}. \] Then we have, for an arbitrary \(G(\mathbb{C}|\mathbb{R})\) -set \(X\) : \[ L _ {X} (s) = L _ {\mathbb {R}} (s) ^ {r _ {1}} L _ {\mathbb {C}} (s) ^ {r _ {2}}. \]

Not formalized. The checked analytic libraries do not package Neukirch’s G(C/R)-set gamma/L-factor formalism with all norm and determinant identities in this source unit.

Proposition (4.3)

FC09-C07-U050 · Chapter VII, §4, source L19256 · not formalized

(4.3) Proposition. (i) \(L_{\mathbb{R}}(1) = 1, L_{\mathbb{C}}(1) = \frac{1}{\pi}\) . (ii) \(L_{\mathbb{R}}(s + 2) = \frac{s}{2\pi} L_{\mathbb{R}}(s), L_{\mathbb{C}}(s + 1) = \frac{s}{2\pi} L_{\mathbb{C}}(s).\) \[ \text {(iii)} L _ {\mathbb {R}} (1 - s) L _ {\mathbb {R}} (1 + s) = \frac {1}{\cos \pi s / 2}, \quad L _ {\mathbb {C}} (s) L _ {\mathbb {C}} (1 - s) = \frac {2}{\sin \pi s}. \] (iv) \(L_{\mathbb{R}}(s)L_{\mathbb{R}}(s + 1) = L_{\mathbb{C}}(s)\) (Legendre’s duplication formula).

Not formalized. The checked analytic libraries do not package Neukirch’s G(C/R)-set gamma/L-factor formalism with all norm and determinant identities in this source unit.

Proposition (4.4)

FC09-C07-U051 · Chapter VII, §4, source L19268 · not formalized

(4.4) Proposition. \(L_{X}(s) = A(s)L_{X}(1 - s)\) with the factor \[ A (s) = (\cos \pi s / 2) ^ {r _ {1} + r _ {2}} (\sin \pi s / 2) ^ {r _ {2}} L _ {\mathbb {C}} (s) ^ {n}. \]

Not formalized. The checked analytic libraries do not package Neukirch’s G(C/R)-set gamma/L-factor formalism with all norm and determinant identities in this source unit.

Definition (5.1)

FC09-C07-U052 · Chapter VII, §5, source L19294 · in Mathlib

(5.1) Definition. The Dedekind zeta function of the number field \(K\) is defined by the series \[ \zeta_ {K} (s) = \sum_ {\mathfrak {a}} \frac {1}{\mathfrak {N} (\mathfrak {a}) ^ {s}}, \] where \(\mathfrak{a}\) varies over the integral ideals of \(K\) , and \(\mathfrak{N}(\mathfrak{a})\) denotes their absolute norm.

Formalized. Mathlib/NumberTheory/NumberField/DedekindZeta.lean::def dedekindZeta — Mathlib groups integral ideals by absolute norm and uses their finite cardinalities as L-series coefficients. Regrouping the source ideal sum by norm gives exactly this Dedekind zeta definition.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (5.2)

FC09-C07-U053 · Chapter VII, §5, source L19302 · in another Lean project

(5.2) Proposition. The series \(\zeta_K(s)\) converge absolutely and uniformly in the domain \(\operatorname{Re}(s) \geq 1 + \delta\) for every \(\delta > 0\) , and one has \[ \zeta_ {K} (s) = \prod_ {\mathfrak {p}} \frac {1}{1 - \mathfrak {N} (\mathfrak {p}) ^ {- s}}, \] where \(\mathfrak{p}\) runs through the prime ideals of \(K\) .

Formalized. Vilin97/lean-pool@c8ddda0a64f21cb019720cdda48c94354d4091e7/LeanPool/Odlyzko/DedekindZeta/IdealSeries.lean::summable_norm_idealInverseNormPower, hasSum_idealInverseNormPower; Vilin97/lean-pool@c8ddda0a64f21cb019720cdda48c94354d4091e7/LeanPool/Odlyzko/DedekindZeta/PrimeIdealEulerProduct.lean::dedekindZeta_primeIdeal_eulerProduct_hasProd; Vilin97/lean-pool@c8ddda0a64f21cb019720cdda48c94354d4091e7/LeanPool/Odlyzko/DedekindZeta/PrimePowerExpansion.lean::multipliableLocallyUniformlyOn_primeIdealFactor; Mathlib/Analysis/Normed/Group/FunctionSeries.lean::tendstoUniformlyOn_tsum — lean-pool proves the literal integral-ideal series and the exact product over prime ideals, including locally uniform multiplicative control. On Re(s)≥1+δ its norm-majorant at 1+δ plus Mathlib’s uniform M-test gives Neukirch’s global uniform convergence statement.

Searched: R=c8ddda0a64f21cb019720cdda48c94354d4091e7 (Mathlib pin de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11, Apache-2.0); P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C07-U054 · Chapter VII, §5, source L19326 · not formalized

The functional equation is then proved for the individual functions \(\zeta(\mathfrak{K}, s)\) . The integral ideals in \(\mathfrak{K}\) are described as follows. If \(a\) is a fractional ideal, then the unit group \(\mathcal{O}^*\) of \(\mathcal{O}\) operates on the set \(a^* = a \setminus \{0\}\) , and we denote by \(a^*/\mathcal{O}^*\) the set of orbits, i.e., the set of classes of non-zero associated elements in \(a\) .

Not formalized. Pinned Mathlib and external Dedekind-zeta developments provide ideal series, Euler products, class-number residues, and a general completed functional equation, but this full row requires a partial-zeta/ideal-class Mellin package, exact Neukirch normalization, general cyclotomic factorization, or another bundled conclusion not exported as one checked owner.

Lemma (5.3)

FC09-C07-U055 · Chapter VII, §5, source L19328 · not formalized

(5.3) Lemma. Let \(\mathfrak{a}\) be an integral ideal of \(K\) and \(\mathfrak{K}\) the class of the ideal \(\mathfrak{a}^{-1}\) . Then there is a bijection \[ \mathfrak {a} ^ {*} / \mathcal {O} ^ {*} \stackrel {{\sim}} {{\longrightarrow}} \left\{\mathfrak {b} \in \mathfrak {K} \mid \mathfrak {b} \text { integral } \right\}, \quad \bar {a} \longmapsto \mathfrak {b} = a \mathfrak {a} ^ {- 1}. \]

Proposition (5.4)

FC09-C07-U056 · Chapter VII, §5, source L19350 · not formalized

(5.4) Proposition. \(\zeta(\mathfrak{K},s) = \mathfrak{N}(\mathfrak{a})^s\sum_{\overline{a}\in \mathfrak{a}^* /\mathcal{O}^*}\frac{1}{|N(\overline{a})|^s}.\)

Definition / construction

FC09-C07-U057 · Chapter VII, §5, source L19352 · after FC09-C01-U048, FC09-C07-U053 · not formalized

By chap. I, (5.2), the ideal \(\mathfrak{a}\) forms a complete lattice in \(\mathbf{R}\) whose fundamental mesh has volume \[ \operatorname{vol} (\mathfrak {a}) = \sqrt {d _ {\mathfrak {a}}}, \] where \(d_{\mathfrak{a}} = \mathfrak{N}(\mathfrak{a})^{2}|d_{K}|\) denotes the absolute value of the discriminant of \(\mathfrak{a}\) , and \(d_{K}\) is the discriminant of \(K\) . To the series \(\zeta(\mathfrak{K}, s)\) we associate the theta series \[ \theta (\mathfrak {a}, z) = \theta_ {\mathfrak {a}} (z / d _ {\mathfrak {a}} ^ {1 / n}) = \sum_ {a \in \mathfrak {a}} e ^ {\pi i \langle a z / d _ {\mathfrak {a}} ^ {1 / n}, a \rangle}. \] It is related to \(\zeta(\mathcal{K},s)\) via the gamma integral associated to the \(G(\mathbb{C}|\mathbb{R})\) -set \(X=\operatorname{Hom}(K,\mathbb{C})\) , \[ \Gamma_ {K} (s) = \Gamma_ {X} (s) = \int_ {\mathbf {R} _ {+} ^ {*}} N (e ^ {- y} y ^ {s}) \frac {d y}{y}, \]

Definition / construction

FC09-C07-U058 · Chapter VII, §5, source L19394 · not formalized

Swapping summation and integration is legal, for the same reason as in the case of the Riemann zeta function (see p. 422). We view the function \[ Z _ {\infty} (s) = | d _ {K} | ^ {s / 2} \pi^ {- n s / 2} \Gamma_ {K} (s / 2) = | d _ {K} | ^ {s / 2} L _ {X} (s) \] as the “Euler factor at infinity” of the zeta function \(\zeta(\mathcal{K}, s)\) (see §4, p. 455) and define \[ Z (\mathfrak {K}, s) = Z _ {\infty} (s) \zeta (\mathfrak {K}, s). \]

Proposition (5.5)

FC09-C07-U059 · Chapter VII, §5, source L19442 · not formalized

(5.5) Proposition. The function \(Z(\mathfrak{K}, 2s)\) is the Mellin transform \[ Z (\mathfrak {K}, 2 s) = L (f, s) \] of the function \[ f (t) = f _ {F} (\mathfrak {a}, t) = \frac {1}{w} \int_ {F} \theta (\mathfrak {a}, i x t ^ {1 / n}) d ^ {*} x, \] where \(w = \# \mu(K)\) denotes the number of roots of unity in \(K\) .

Lemma (5.6)

FC09-C07-U060 · Chapter VII, §5, source L19482 · after FC09-C01-U060 · not formalized

(5.6) Lemma. The fundamental domain \(F\) of \(S\) has the following volume with respect to \(d^{*}x\) : \[ \operatorname{vol} (F) = 2 ^ {r - 1} R, \] where r is the number of infinite places and R is the regulator of K (see chap. I, (7.5)).

Lemma (5.7)

FC09-C07-U061 · Chapter VII, §5, source L19538 · not formalized

(5.7) Lemma. The lattice \(\Gamma'\) in \(\mathbf{R}\) which is dual to the lattice \(\Gamma = \mathfrak{a}\) is given by \[ { } ^ { * } \Gamma ^ { \prime } = ( \mathfrak { a d } ) ^ { - 1 } , \] where the asterisk denotes the involution \((x_{\tau}) \mapsto (\overline{x}_{\tau})\) on \(K_{R}\) and d the different of \(K|Q\) .

Proposition (5.8)

FC09-C07-U062 · Chapter VII, §5, source L19560 · not formalized

(5.8) Proposition. The functions \(f_{F}(\mathfrak{a}, t)\) satisfy the transformation formula \[ f _ {F} \left(\mathfrak {a}, \frac {1}{t}\right) = t ^ {1 / 2} f _ {F ^ {- 1}} \left((\mathfrak {a d}) ^ {- 1}, t\right), \] and one has \[ f _ {F} (\mathfrak {a}, t) = \frac {2 ^ {r - 1}}{w} R + O (e ^ {- c t ^ {1 / n}}) \quad \text { for } t \to \infty , c > 0. \]

Theorem (5.9)

FC09-C07-U063 · Chapter VII, §5, source L19636 · not formalized

(5.9) Theorem. The function \[ Z (\mathfrak {K}, s) = Z _ {\infty} (s) \zeta (\mathfrak {K}, s), \quad \operatorname{Re} (s) > 1, \] \(Z_{\infty}(s) = |d_K|^{s / 2}\pi^{-ns / 2}\Gamma_K(s / 2)\) , admits an analytic continuation to \(\mathbb{C} \setminus \{0,1\}\) and satisfies the functional equation \[ Z (\mathfrak {K}, s) = Z \left(\mathfrak {K} ^ {\prime}, 1 - s\right), \] where the ideal classes \(\mathfrak{K}\) and \(\mathfrak{K}'\) correspond to each other via \(\mathfrak{K}\mathfrak{K}' = [\mathfrak{d}]\) . It has simple poles at \(s = 0\) and \(s = 1\) with residues \[ - \frac {2 ^ {r}}{w} R, \quad r e s p. \frac {2 ^ {r}}{w} R. \]

Corollary (5.10)

FC09-C07-U064 · Chapter VII, §5, source L19696 · not formalized

(5.10) Corollary. The completed zeta function \(Z_{K}(s)\) admits an analytic continuation to C \(\setminus\{0,1\}\) and satisfies the functional equation \[ Z _ {K} (s) = Z _ {K} (1 - s). \] It has simple poles at \(s = 0\) and \(s = 1\) with residues \[ - \frac {2 ^ {r} h R}{w}, \quad r e s p. \frac {2 ^ {r} h R}{w}, \] where \(h\) is the class number of \(K\) .

Corollary (5.11)

FC09-C07-U065 · Chapter VII, §5, source L19762 · after FC09-C03-U058, FC09-C07-U044 · not formalized

(5.11) Corollary. (i) The Dedekind zeta function \(\zeta_K(s)\) has an analytic continuation to \(\mathbb{C} \setminus \{1\}\) . (ii) At \(s = 1\) it has a simple pole with residue \[ \kappa = \frac {2 ^ {r _ {1}} (2 \pi) ^ {r _ {2}}}{w | d _ {K} | ^ {1 / 2}} h R = h R / e ^ {g}. \] Here h denotes the class number and \[ g = \log \frac {w | d _ {K} | ^ {1 / 2}}{2 ^ {r _ {1}} (2 \pi) ^ {r _ {2}}} \] the genus of the number field \(K\) (see chap. III, (3.5)). (iii) It satisfies the functional equation \[ \zeta_ {K} (1 - s) = A (s) \zeta_ {K} (s) \] with the factor \[ A (s) = \left| d _ {K} \right| ^ {s - \frac {1}{2}} \left(\cos \frac {\pi s}{2}\right) ^ {r _ {1} + r _ {2}} \left(\sin \frac {\pi s}{2}\right) ^ {r _ {2}} L _ {\mathbb {C}} (s) ^ {n}. \]

Proposition (5.12)

FC09-C07-U066 · Chapter VII, §5, source L19802 · not formalized

(5.12) Proposition. If \(K = \mathbb{Q}(\mu_m)\) is the field of \(m\) -th roots of unity, then \[ \zeta_ {K} (s) = G (s) \prod_ {\chi} L (\chi , s), \] where \(\chi\) varies over all Dirichlet characters mod m, and \[ G (s) = \prod_ {\mathfrak {p} | m} (1 - \mathfrak {N} (\mathfrak {p}) ^ {- s}) ^ {- 1}. \]

Proposition (5.13)

FC09-C07-U067 · Chapter VII, §5, source L19842 · in Mathlib

(5.13) Proposition. For every non-trivial Dirichlet character \(\chi\) , one has \[ L (\chi , 1) \neq 0. \]

Formalized. Mathlib/NumberTheory/LSeries/Nonvanishing.lean::LFunction_apply_one_ne_zero — This is exactly the nonvanishing theorem used by Neukirch before deriving primes in arithmetic progressions.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Dirichlet’s Prime Number Theorem (5.14)

FC09-C07-U068 · Chapter VII, §5, source L19850 · in Mathlib

(5.14) Dirichlet’s Prime Number Theorem. Every arithmetic progression \[ a, a \pm m, a \pm 2 m, a \pm 3 m, \dots , \text { with } (a, m) = 1, \] i.e., every class a mod m, contains infinitely many prime numbers.

Formalized. Mathlib/NumberTheory/LSeries/PrimesInAP.lean::infinite_setOfPred_prime_and_eq_mod, exists_prime_gt_and_zmodEq — Pinned Mathlib proves infinitude, and equivalently arbitrarily large primes, in every reduced residue class modulo N; this is Neukirch’s Theorem 5.14.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U069 · Chapter VII, §6, source L19888 · not formalized

Let \(m\) be an integral ideal of the number field \(K\) , and let \(J^m\) be the group of all ideals of \(K\) which are relatively prime to \(m\) . Given any character \[ \chi : J ^ {\mathfrak {m}} \rightarrow S ^ {1} = \left\{z \in \mathbb {C} \mid | z | = 1 \right\}, \] we may associate to it, as a common generalization of the Dirichlet L-series as well as the Dedekind zeta function, the L-series \[ L (\chi , s) = \sum_ {\mathfrak {a}} \frac {\chi (\mathfrak {a})}{\mathfrak {N} (\mathfrak {a}) ^ {s}}. \] Here \(\mathfrak{a}\) varies over all integral ideals of \(K\) , and one defines \(\chi(\mathfrak{a}) = 0\) whenever \((\mathfrak{a}, \mathfrak{m}) \neq 1\) . Searching for the most comprehensive class of characters \(\chi\) for which the corresponding \(L\) -series could be shown to have a functional equation, HECKE was led to the notion of Größencharaktere, which we define as follows.

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition (6.1)

FC09-C07-U070 · Chapter VII, §6, source L19902 · not formalized

(6.1) Definition. A Größencharakter mod m is a character \(\chi: J^{m} \to S^{1}\) for which there exists a pair of characters \[ \chi_ {\mathrm{f}}: (\mathcal {O} / \mathfrak {m}) ^ {*} \longrightarrow S ^ {1}, \quad \chi_ {\infty}: \mathbf {R} ^ {*} \longrightarrow S ^ {1}, \] such that \[ \chi ((a)) = \chi_ {\mathrm{f}} (a) \chi_ {\infty} (a) \] for every algebraic integer \(a \in \mathcal{O}\) relatively prime to \(\mathfrak{m}\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Convention / notation

FC09-C07-U071 · Chapter VII, §6, source L19928 · not formalized

From \[ \mathcal {O} ^ {(\mathfrak {m})} = \left\{a \in \mathcal {O} \mid (a, \mathfrak {m}) = 1 \right\}, \] it extends uniquely to the group \[ K ^ {(\mathfrak {m})} = \left\{a \in K ^ {*} \mid (a, \mathfrak {m}) = 1 \right\} \] of all fractions relatively prime to m, because every \(a \in K^{(m)}\) determines a well-defined class in \((\mathcal{O}/\mathfrak{m})^{*}\) . The character \(\chi_{\infty}\) , and thus also the character \(\chi_{f}\) , are determined uniquely by the Größencharakter \(\chi\) , since the group \[ K ^ {\mathfrak {m}} = \left\{a \in K ^ {(\mathfrak {m})} \mid a \equiv 1 \bmod \mathfrak {m} \right\} \] is dense in \(\mathbf{R}^*\) , by the approximation theorem, and one has \(\chi_{\infty}(a) = \chi((a))\) for \(a \in K^{\mathfrak{m}}\) . Let us recall that the congruence \(a \equiv 1 \mod \mathfrak{m}\) signifies that \(a = b/c\) , for two integers \(b, c\) relatively prime to \(\mathfrak{m}\) , such that \(b \equiv c \mod \mathfrak{m}\) or, equivalently, \(a \in U_{\mathfrak{p}}^{(n_{\mathfrak{p}})} \subseteq K_{\mathfrak{p}}\) for \(\mathfrak{p}|\mathfrak{m}\) , if \(\mathfrak{m} = \prod_{\mathfrak{p}} \mathfrak{p}^{n_{\mathfrak{p}}}\) . The character \(\chi_{\infty}\) factors automatically through \(R^{*}/O^{m}\) , where \[ \mathcal {O} ^ {\mathfrak {m}} = \left\{\varepsilon \in \mathcal {O} ^ {*} \mid \varepsilon \equiv 1 \bmod \mathfrak {m} \right\}. \] In fact, for \(\varepsilon \in \mathcal{O}^{\mathfrak{m}}\) we have \(\chi_{\mathrm{f}}(\varepsilon) = 1\) , and thus \(\chi_{\infty}(\varepsilon) = \chi_{\mathrm{f}}(\varepsilon)\chi_{\infty}(\varepsilon) = \chi((\varepsilon)) = 1\) . The two characters \(\chi_{\mathrm{f}}\) and \(\chi_{\infty}\) of \((\mathcal{O}/\mathfrak{m})^{*}\) , resp. \(\mathbf{R}^{*}/\mathcal{O}^{\mathfrak{m}}\) , associated with a Größencharakter \(\chi\) satisfy the relation \[ \chi_ {\mathrm{f}} (\varepsilon) \chi_ {\infty} (\varepsilon) = 1 \quad \text { for all } \varepsilon \in \mathcal {O} ^ {*}, \] and it can be shown that every such pair of characters \((\chi_{\mathrm{f}}, \chi_{\infty})\) comes from a Größencharakter \(\chi\) (exercise 5).

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Proposition (6.2)

FC09-C07-U072 · Chapter VII, §6, source L19964 · not formalized

(6.2) Proposition. Let \(\chi\) be a Größencharakter mod \(\mathfrak{m}\) , and let \(\mathfrak{m}'\) be a divisor of \(\mathfrak{m}\) . Then the following conditions are equivalent. (i) \(\chi\) is the restriction of a Größencharakter \(\chi': J^{\mathfrak{m}'} \to S^1 \bmod \mathfrak{m}'\) . (ii) \(\chi_{\mathrm{f}}\) factors through \((\mathcal{O} / \mathfrak{m}')^{*}\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition / construction

FC09-C07-U073 · Chapter VII, §6, source L20004 · after FC09-C07-U072 · not formalized

The Größencharakter \(\chi \mod m\) is called primitive if it is not the restriction of a Größencharakter \(\chi' \mod m'\) for any proper divisor \(m'|m\) . According to (6.2), this is the case if and only if the character \(\chi_{f}\) of \((\mathcal{O}/\mathfrak{m})^{*}\) is primitive in the sense that it does not factorize through \((\mathcal{O}/\mathfrak{m}')^{*}\) for any proper divisor \(m'|m\) . The conductor of \(\chi\) is the smallest divisor f of m such that \(\chi\) is the restriction of a Größencharakter mod f. By (6.2), f is the conductor of \(\chi_{f}\) , i.e., the smallest divisor of m such that \(\chi_{f}\) factors through \((\mathcal{O}/\mathfrak{f})^{*}\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition (6.3)

FC09-C07-U074 · Chapter VII, §6, source L20010 · not formalized

(6.3) Definition. Let \(\chi_{\mathrm{f}}\) be a character of \((\mathcal{O} / \mathfrak{m})^{*}\) and \(y\in \mathfrak{m}^{-1}\mathfrak{d}^{-1}\) , where \(\mathfrak{d}\) is the different of \(K|\mathbb{Q}\) . Then we define the Gauss sum of \(\chi_{\mathrm{f}}\) to be \[ \tau_{\mathfrak{m}}(\chi_{\mathrm{f}},y) = \sum_{\substack{x\bmod \mathfrak{m}\\ (x,\mathfrak{m}) = 1}}\chi_{\mathrm{f}}(x)e^{2\pi i Tr(xy)}, \] where \(x\) varies over a system of representatives of \((\mathcal{O} / \mathfrak{m})^{*}\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Theorem (6.4)

FC09-C07-U075 · Chapter VII, §6, source L20026 · not formalized

(6.4) Theorem. Let \(\chi_{\mathrm{f}}\) be a primitive character of \((\mathcal{O} / \mathfrak{m})^{*}\) , let \(y \in \mathfrak{m}^{-1}\mathfrak{d}^{-1}\) and \(a \in \mathcal{O}\) . Then one has \[ \tau_ {\mathfrak {m}} (\chi_ {\mathrm{f}}, a y) = \left\{ \begin{array}{l l} \overline {{\chi}} _ {\mathrm{f}} (a) \tau_ {\mathfrak {m}} (\chi_ {\mathrm{f}}, y), & i f (a, \mathfrak {m}) = 1, \\ 0, & i f (a, \mathfrak {m}) \neq 1, \end{array} \right. \] and furthermore \[ \left| \tau_ {\mathfrak {m}} (\chi_ {\mathrm{f}}, y) \right| = \sqrt {\mathfrak {N} (\mathfrak {m})}, \quad i f (y \mathfrak {m} \mathfrak {d}, \mathfrak {m}) = 1. \]

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Proposition (6.5)

FC09-C07-U076 · Chapter VII, §6, source L20046 · not formalized

(6.5) Proposition. If \(\mathfrak{a} \neq 1\) , then \(\sum_{\mathfrak{b} \mid \mathfrak{a}} \mu(\mathfrak{b}) = 0\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Lemma (6.6)

FC09-C07-U077 · Chapter VII, §6, source L20062 · not formalized

(6.6) Lemma. One has \[ T _ {1} (y) = \sum_ {\mathfrak {a} | \mathfrak {m}} \mu (\mathfrak {a}) S _ {\mathfrak {a}} (y), \] and for every divisor \(\mathfrak{a}|\mathfrak{m}\) , \[ S _ {\mathfrak {a}} (y) = \left\{ \begin{array}{l l} \mathfrak {N} (\frac {\mathfrak {m}}{\mathfrak {a}}), & i f y \in \mathfrak {a} ^ {- 1} \mathfrak {d} ^ {- 1}, \\ 0, & i f y \notin \mathfrak {a} ^ {- 1} \mathfrak {d} ^ {- 1}. \end{array} \right. \]

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Proposition (6.7)

FC09-C07-U078 · Chapter VII, §6, source L20136 · not formalized

(6.7) Proposition. The characters \(\lambda\) of \(\mathbf{R}^*\) , i.e., the continuous homomorphisms \[ \lambda : \mathbf {R} ^ {*} \longrightarrow S ^ {1}, \] are given explicitly by \[ \lambda (x) = N \left(x ^ {p} | x | ^ {- p + i q}\right), \] for some admissible \(p \in \prod_{\tau} \mathbb{Z}\) (see §3, p.448) and a \(q \in \mathbf{R}_{\pm}\) . \(p\) and \(q\) are uniquely determined by \(\lambda\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition / construction

FC09-C07-U079 · Chapter VII, §6, source L20196 · not formalized

If the character \(\chi_{\infty}\) associated to the Größencharakter \(\chi: J^{\mathfrak{m}} \to S^{1}\) is given by \[ \chi_ {\infty} (x) = N \left(x ^ {p} | x | ^ {- p + i q}\right), \] then we say that \(\chi\) is of type \((p,q)\) , and we call \(p - iq\) the exponent of \(\chi\) . Since \(\chi_{\infty}\) factors through \(\mathbf{R}^{*} / \mathcal{O}^{\mathfrak{m}}\) , not all exponents actually occur (see exercise 3).

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition (6.8)

FC09-C07-U080 · Chapter VII, §6, source L20218 · not formalized

(6.8) Definition. A Dirichlet character mod m is a character \[ \chi : J ^ {\mathfrak {m}} / P ^ {\mathfrak {m}} \longrightarrow S ^ {1} \] of the ray class group mod m, i.e., a character \(\chi : J^{\mathfrak{m}} \to S^{1}\) such that \(\chi(P^{\mathfrak{m}}) = 1\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition / construction

FC09-C07-U081 · Chapter VII, §6, source L20226 · not formalized

The conductor of a Dirichlet character \(\chi\) mod \(\mathfrak{m}\) is defined to be the smallest module \(f\) dividing \(\mathfrak{m}\) such that \(\chi\) factors through \(J^{\mathfrak{f}} / P^{\mathfrak{f}}\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Proposition (6.9)

FC09-C07-U082 · Chapter VII, §6, source L20228 · not formalized

(6.9) Proposition. The Dirichlet characters \(\chi \mod m\) are precisely the Größencharaktere mod m of type \((p,0)\) , \(p = (p_{\tau})\) , such that \(p_{\tau} = 0\) for all complex \(\tau\) . In other words, one has \[ \chi ((a)) = \chi_ {\mathrm{f}} (a) N \biggl (\left(\frac {a}{| a |}\right) ^ {p} \biggr), \] for some character \(\chi_{f}\) of \((\mathcal{O}/\mathfrak{m})^{*}\) . The conductor of the Dirichlet character is at the same time also the conductor of the corresponding Größencharakter.

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Corollary (6.10)

FC09-C07-U083 · Chapter VII, §6, source L20260 · not formalized

(6.10) Corollary. The characters of the ideal class group \(Cl_{K} = J/P\) , i.e., the characters \(\chi : J \to S^{1}\) such that \(\chi(P) = 1\) , are precisely the Größencharaktere \(\chi \mod 1\) satisfying \(\chi_{\infty} = 1\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition (6.11)

FC09-C07-U084 · Chapter VII, §6, source L20272 · not formalized

(6.11) Definition. A Hecke character is a character of the idèle class group \(C = I / K^{*}\) of the number field \(K\) , i.e., a continuous homomorphism \[ \chi : I \longrightarrow S ^ {1} \] of the idèle group \(I = \prod_{\mathfrak{p}} K_{\mathfrak{p}}^{*}\) such that \(\chi(K^{*}) = 1\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition / construction

FC09-C07-U085 · Chapter VII, §6, source L20280 · after FC09-C06-U016, FC09-C07-U013 · not formalized

In order to deal with Hecke characters concretely, consider an integral ideal \(m = \prod_{p} p^{n_{p}}\) of K, i.e., \(n_{p} \geq 0\) and \(n_{p} = 0\) for \(p \mid \infty\) . We associate to this ideal the subgroup \(\bar{I}^{m}\) of I, \[ \bar {I} ^ {\mathfrak {m}} = I _ {\mathrm{f}} ^ {\mathfrak {m}} \times I _ {\infty} \quad \text { where } \quad I _ {\mathrm{f}} ^ {\mathfrak {m}} = \prod_ {\mathfrak {p} \nmid \infty} U _ {\mathfrak {p}} ^ {(n _ {\mathfrak {p}})}, \quad I _ {\infty} = \prod_ {\mathfrak {p} | \infty} K _ {\mathfrak {p}} ^ {*}. \] If \(\mathfrak{p} \nmid \infty\) , then \(U_{\mathfrak{p}}^{(n)}\) is the group of units \(U_{\mathfrak{p}}\) if \(n = 0\) , and the \(n\) -th group of higher units for \(n \geq 1\) . We interpret \(I_{\infty}\) as the multiplicative group \(\mathbf{R}^*\) of the \(\mathbb{R}\) -algebra \(\mathbf{R} = K \otimes_{\mathbb{Q}} \mathbb{R} = \prod_{\mathfrak{p} | \infty} K_{\mathfrak{p}}\) . Observe that \(\bar{I}^{\mathfrak{m}}\) differs slightly from the congruence subgroup \(I^{\mathfrak{m}} = \prod_{\mathfrak{p}} U_{\mathfrak{p}}^{(n_{\mathfrak{p}})}\) introduced in chap. VI, §1, in that, for real \(\mathfrak{p}\) , we have the factor \(U_{\mathfrak{p}}^{(0)} = \mathbb{R}_{+}^{*}\) instead of the component \(K_{\mathfrak{p}}^{*}\) . The effect is that \(I / \bar{I}^{\mathfrak{m}} K^{*}\) is not the ray class group \(J^{\mathfrak{m}} / P^{\mathfrak{m}} \bmod \mathfrak{m}\) , but isomorphic to the quotient \(J^{\mathfrak{m}} / \bar{P}^{\mathfrak{m}}\) by the group \(\bar{P}^{\mathfrak{m}}\) of all principal ideals ( \(a\) ) such that \(a \equiv 1 \bmod \mathfrak{m}\) - this is seen as in chap. VI, (1.9). We will refer to \(J^{\mathfrak{m}} / \bar{P}^{\mathfrak{m}}\) as the small ray class group.

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Definition / construction

FC09-C07-U086 · Chapter VII, §6, source L20288 · not formalized

We call m a module of definition for the Hecke character \(\chi\) if \[ \chi (I _ {\mathrm{f}} ^ {\mathfrak {m}}) = 1. \] Every Hecke character admits a module of definition, since the image of \(\chi : \prod_{\mathfrak{p} \nmid \infty} U_{\mathfrak{p}} \to S^1\) is a compact and totally disconnected subgroup of \(S^1\) , hence finite, and so the kernel has to contain a subgroup of the form \(\prod_{\mathfrak{p} \nmid \infty} U_{\mathfrak{p}}^{(n_{\mathfrak{p}})}\) where \(n_{\mathfrak{p}} = 0\) for almost all \(\mathfrak{p}\) . For it we can take the ideal \(\mathfrak{m} = \prod_{\mathfrak{p} \nmid \infty} \mathfrak{p}^{n_{\mathfrak{p}}}\) as a module of definition.

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Proposition (6.12)

FC09-C07-U087 · Chapter VII, §6, source L20312 · not formalized

(6.12) Proposition. There is an exact sequence \[ 1 \longrightarrow \mathbf {R} ^ {*} / \mathcal {O} ^ {\mathfrak {m}} \longrightarrow C (\mathfrak {m}) \longrightarrow J ^ {\mathfrak {m}} / \bar {P} ^ {\mathfrak {m}} \longrightarrow 1. \]

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Proposition (6.13)

FC09-C07-U088 · Chapter VII, §6, source L20344 · not formalized

(6.13) Proposition. There is a canonical exact sequence \[ 1 \longrightarrow K ^ {(\mathfrak {m})} / \mathcal {O} ^ {\mathfrak {m}} \stackrel {\delta} {\longrightarrow} J ^ {\mathfrak {m}} \times (\mathcal {O} / \mathfrak {m}) ^ {*} \times \mathbf {R} ^ {*} / \mathcal {O} ^ {\mathfrak {m}} \stackrel {f} {\longrightarrow} C (\mathfrak {m}) \longrightarrow 1, \] where \(\delta\) is given by \[ \delta (a) = \left((a) ^ {- 1}, a \bmod \mathfrak {m}, a \bmod \mathcal {O} ^ {\mathfrak {m}}\right). \]

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Corollary (6.14)

FC09-C07-U089 · Chapter VII, §6, source L20450 · not formalized

(6.14) Corollary. The correspondence \(\chi \mapsto \chi \circ c\) is \(1 - 1\) between characters \(\chi\) of \(C(\mathfrak{m})\) , i.e., Hecke characters with module of definition \(\mathfrak{m}\) , and Größencharaktere mod \(\mathfrak{m}\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s general ideal-character/ray-class Größencharacter analytic theory and its special-value consequences for this row.

Proposition (7.1)

FC09-C07-U090 · Chapter VII, §7, source L20506 · not formalized

(7.1) Proposition. There is a commutative exact diagram with a subgroup \(\widehat{K}^* \subseteq \mathbf{C}^*\) containing \(K^*\) such that \(|a| \in \mathbf{R}_+^*\) , and \[ \mathfrak {N} \bigl ((a) \bigr) = \left| N (a) \right| \] for all \(a \in \widehat{K}^*\) .

Not formalized. No checked compatible Lean owner supplies the full ray-class/Hecke character structure, conductor/index comparison, or associated analytic continuation package required by this row.

Definition / construction

FC09-C07-U091 · Chapter VII, §7, source L20518 · not formalized

Let the ideal class group \(J / P\) be given by a basis \([\mathfrak{b}_1], \ldots, [\mathfrak{b}_r]\) , and choose, for every one of these basic classes, an ideal \(\mathfrak{b}_1, \ldots, \mathfrak{b}_r\) . Then every fractional ideal \(\mathfrak{a} \in J\) can be written in the form \[ \mathfrak {a} = a \mathfrak {b} _ {1} ^ {\nu_ {1}} \dots \mathfrak {b} _ {r} ^ {\nu_ {r}} \] where \(a \in K^{*}\) is well-determined up to a unit \(\varepsilon \in \mathcal{O}^{*}\) , and the exponents \(\nu_{i} \mod h_{i}\) are uniquely determined, \(h_{i}\) being the order of \([\mathfrak{b}_i]\) in \(J/P\) . Let \(\mathfrak{b}_i^{h_i} = (b_i)\) . For every \(\tau \in \operatorname{Hom}(K, \mathbb{C})\) , we choose a fixed root \[ \widehat {b} _ {i \tau} = \sqrt [ h _ {i} ]{\tau b _ {i}} \] in \(\mathbb{C}\) in such a way that \(\widehat{b}_{i\overline{\tau}} = \widehat{b}_{i\tau}\) whenever \(\tau\) is complex. We define \(\widehat{K}^*\) to be the subgroup of \(\mathbf{C}^*\) generated by \(K^*\) and by the elements \(\widehat{b}_i = (\widehat{b}_{i\tau})\in \mathbf{C}^*\) . Each class \([\mathfrak{b}]\in J / P\) contains a uniquely determined ideal of the form \[ \mathfrak {b} = \mathfrak {b} _ {1} ^ {\nu_ {1}} \dots \mathfrak {b} _ {r} ^ {\nu_ {r}} \quad \text { with } \quad 0 \leq \nu_ {i} < h _ {i}, \] and we consider the mapping \[ f: J / P \longrightarrow \widehat {K} ^ {*} / K ^ {*}, \quad f ([ \mathfrak {b} ]) = \widehat {b} _ {1} ^ {\nu_ {1}} \dots \widehat {b} _ {r} ^ {\nu_ {r}} \bmod K ^ {*}. \] It is a homomorphism, for if \(\mathfrak{b} = \mathfrak{b}_1^{\nu_1}\dots \mathfrak{b}_r^{\nu_r}\) and \(\mathfrak{b}' = \mathfrak{b}_1^{\nu_1'}\dots \mathfrak{b}_r^{\nu_r'}\) , and if \(\nu_{i} + \nu_{i}' = \mu_{i} + \lambda_{i}h_{i}, 0\leq \mu_{i} < h_{i}\) , then \(\mathfrak{b}_1^{\mu_1}\dots \mathfrak{b}_r^{\mu_r}\) is the ideal belonging to the class \([\mathfrak{b}][\mathfrak{b}']\) , and \[ \begin{array}{c} f ([ \mathfrak {b} ] [ \mathfrak {b} ^ {\prime} ]) = \widehat {b} _ {1} ^ {\mu_ {1}} \dots \widehat {b} _ {r} ^ {\mu_ {r}} \equiv \widehat {b} _ {1} ^ {\mu_ {1}} \dots \widehat {b} _ {r} ^ {\mu_ {r}} b _ {1} ^ {\lambda_ {1}} \dots b _ {r} ^ {\lambda_ {r}} \\ \equiv (\widehat {b} _ {1} ^ {\nu_ {1}} \dots \widehat {b} _ {r} ^ {\nu_ {r}}) (\widehat {b} _ {1} ^ {\nu_ {1} ^ {\prime}} \dots \widehat {b} _ {r} ^ {\nu_ {r} ^ {\prime}}) \text {mod} K ^ {*} = f ([ \mathfrak {b} ]) f ([ \mathfrak {b} ^ {\prime} ]). \end{array} \] f is clearly surjective. To show the injectivity, let \(\widehat{b}_{1}^{\nu_{1}}\cdots\widehat{b}_{r}^{\nu_{r}}=a\in K^{*}\) , and let \(h=h_{1}\cdots h_{r}\) be the class number of K. Then we have for the ideal \(a = a^{-1}b_{1}^{\nu_{1}} \cdots b_{r}^{\nu_{r}} \in J\) that \(a^{h} = a^{-h}(b_{1}^{\nu_{1}h/h_{1}} \cdots b_{r}^{\nu_{r}h/h_{r}}) = a^{-h}(\widehat{b}_{1}^{\nu_{1}} \cdots \widehat{b}_{r}^{\nu_{r}})^{h} = (1)\) . Since J is torsion-free, it follows that \(a = (1)\) , and so \(b_{1}^{\nu_{1}} \cdots b_{r}^{\nu_{r}} = (a) \in P\) . From this we deduce that every element \(\widehat{a} \in \widehat{K}^{*}\) admits a unique representation \[ \widehat{a} = a\,\widehat{b}_{1}^{\nu_{1}} \cdots \widehat{b}_{r}^{\nu_{r}}, \quad 0 \leq \nu_{i} < h_{i}, \quad a \in K^{*}. \]

Definition / construction

FC09-C07-U092 · Chapter VII, §7, source L20554 · not formalized

We define a map \[ (\quad): \widehat {K} ^ {*} \longrightarrow J \] by \[ \widehat {a} = a \widehat {b} _ {1} ^ {\nu_ {1}} \dots \widehat {b} _ {r} ^ {\nu_ {r}} \longmapsto (\widehat {a}) = a \mathfrak {b} _ {1} ^ {\nu_ {1}} \dots \mathfrak {b} _ {r} ^ {\nu_ {r}}. \] Arguing as above, we see that this is a homomorphism. It is surjective and obviously has kernel \(\mathcal{O}^*\) . Finally we have that \(|\widehat{b_i}| = (|\widehat{b_{i\tau}}|) \in \mathbf{R}_+^*\) and \[ \mathfrak {N} \big ((\widehat {b _ {i}}) \big) ^ {h _ {i}} = \mathfrak {N} (\mathfrak {b} _ {i} ^ {h _ {i}}) = \left| N (b _ {i}) \right| = \left| \prod_ {\tau} \tau b _ {i} \right| = \left| \prod_ {\tau} \widehat {b} _ {i \tau} ^ {h _ {i}} \right| = \left| N (\widehat {b _ {i}}) \right| ^ {h _ {i}}, \] so that \(\mathfrak{N}((\widehat{b}_i)) = |N(\widehat{b}_i)|\) , and thus \(|a| \in \mathbf{R}_+^*\) , \(\mathfrak{N}((a)) = |N(a)|\) for all \(a \in \widehat{K}^*\) .

Convention / notation

FC09-C07-U093 · Chapter VII, §7, source L20574 · after FC09-C07-U090 · not formalized

The elements \(a\) of \(\widehat{K}^*\) used to be called ideal numbers - a name which is somewhat forgotten but will be used in what follows. The diagram (7.1) implies an isomorphism \[ \widehat {K} ^ {*} / K ^ {*} \cong J / P. \] For \(a, b \in \widehat{K}^*\) we write \(a \sim b\) if \(a\) and \(b\) lie in the same class, i.e., if \(ab^{-1} \in K^*\) . We call \(a\) an ideal integer, or an integral ideal number, if (a) is an integral ideal. The semigroup of all ideal integers will be denoted by \(\widehat{\mathcal{O}}\) . Furthermore we write \(a \mid b\) if \(\frac{b}{a} \in \widehat{\mathcal{O}}\) , and for every pair \(a, b \in \widehat{K}^*\) , we have the notion of \(\gcd(a, b) \in \widehat{K}^*\) (which is lacking inside \(K^*\) ). The greatest common divisor is the ideal number \(d\) (which is unique up to a unit) such that the ideal (d) is the gcd of the ideals (a), (b). Observe that the ideal numbers are not defined in a canonical way. This is the reason why they have not been able to hold their own in the development of number theory. (They are treated in [46], [65].)

Convention / notation

FC09-C07-U094 · Chapter VII, §7, source L20582 · not formalized

We now form an analogous extension of the prime residue groups \((\mathbb{Z}/m\mathbb{Z})^{*}\) . For three ideal numbers a, b, m, the congruence \[ a \equiv b \bmod m \] signifies that \(a \sim b\) and \(\frac{a-b}{m} \in \widehat{\mathcal{O}} \cup \{0\}\) . If \(\mathfrak{m} = (m)\) , we also write this relation as \(a \equiv b \mod \mathfrak{m}\) . Let \(\mathfrak{m}\) be an integral ideal. The semigroup \(\widehat{\mathcal{O}}^{(\mathfrak{m})}\) of all integral ideal numbers relatively prime to \(\mathfrak{m}\) is partitioned by the equivalence relation \(\equiv\) into classes, which we will write as \(a \mod \mathfrak{m}\) . They are given explicitly as follows.

Lemma (7.2)

FC09-C07-U095 · Chapter VII, §7, source L20590 · not formalized

(7.2) Lemma. For every \(a \in \widehat{\mathcal{O}}^{(\mathfrak{m})}\) one has \[ a \bmod {\mathfrak {m}} = a + a (a ^ {- 1}) {\mathfrak {m}}. \]

Proposition (7.3)

FC09-C07-U096 · Chapter VII, §7, source L20612 · not formalized

(7.3) Proposition. \((\widehat{\mathcal{O}} / \mathfrak{m})^{*}\) is an abelian group, and we have a canonical exact sequence \[ 1 \longrightarrow (\mathcal {O} / \mathfrak {m}) ^ {*} \longrightarrow (\widehat {\mathcal {O}} / \mathfrak {m}) ^ {*} \longrightarrow J / P \longrightarrow 1. \]

Convention / notation

FC09-C07-U097 · Chapter VII, §7, source L20622 · not formalized

For an ideal class \(\mathcal{K} \in J / P\) , we will denote by \(\mathcal{K}' \in J / P\) in what follows the class defined by \[ \mathcal {K} \mathcal {K} ^ {\prime} = [ \mathfrak {m d} ], \] where \(\mathfrak{d}\) is the different of \(K|\mathbb{Q}\) . Let \(\mathfrak{m} = (m)\) and \(\mathfrak{d} = (d)\) , with some fixed ideal numbers \(m, d\) . For \(\mathfrak{m} = \mathcal{O}\) let \(m = 1\) . We now study characters \[ \chi : (\widehat {\mathcal {O}} / \mathfrak {m}) ^ {*} \longrightarrow \mathbb {C} ^ {*}, \] and put \(\chi(a)=0\) for \(a\in\mathcal{O}\) such that \((a,\mathfrak{m})\neq1\) . In the applications, \(\chi\) will come from a Größencharakter mod m, but the treatment of the theta series is independent of such an origin of \(\chi\) .

Definition (7.4)

FC09-C07-U098 · Chapter VII, §7, source L20636 · not formalized

(7.4) Definition. Let \(a \in \widehat{\mathcal{O}}\) be an ideal integer, and let \(\mathcal{K}\) be the class of \((a)\) . Then we define the Gauss sum \[ \tau (\chi , a) = \sum_ {\hat {x} \bmod m} \chi (\widehat {x}) e ^ {2 \pi i T r (\hat {x} a / m d)}, \] where \(\widehat{x}\) mod m runs through the classes of \((\widehat{\mathcal{O}}/\mathfrak{m})^{*}\) which are mapped to the class \(K'\) . In particular, we put \(\tau(\chi)=\tau(\chi,1)\) .

Proposition (7.5)

FC09-C07-U099 · Chapter VII, §7, source L20676 · not formalized

(7.5) Proposition. For a primitive character \(\chi\) of \((\widehat{\mathcal{O}}/\mathfrak{m})^{*}\) , one has \[ \tau (\chi , a) = \overline {{\chi}} (a) \tau (\chi) \] and \(|\tau (\chi)| = \sqrt{\mathfrak{N}(\mathfrak{m})}\) .

Definition / construction

FC09-C07-U100 · Chapter VII, §7, source L20684 · after FC09-C07-U045 · not formalized

The theta series \(\theta(\chi, z)\) used in §2 in the treatment of Dirichlet \(L\) -series are attached to the field \(\mathbb{Q}\) . We now have to find their analogues relative to an arbitrary number field \(K\) . Given any admissible element \(p \in \prod_{\tau} \mathbb{Z}\) (see §3, p.448) and a character \(\chi\) of \((\widehat{\mathcal{O}}/\mathfrak{m})^*\) , we form the Hecke theta series \[ \theta^ {p} (\chi , z) = \sum_ {a \in \hat {\mathcal {O}} \cup \{0 \}} \chi (a) N (a ^ {p}) e ^ {\pi i \langle a z / | m d |, a \rangle}, \] where m, d are fixed ideal numbers such that \((m) = \mathfrak{m}\) and \((d) = \mathfrak{d}\) . We take m = 1 if \(\mathfrak{m} = 1\) . The case \(\mathfrak{m} = 1\) , p = 0 is exceptional in that the constant term of the theta series is \(\chi(0)N(0^{p}) = 1\) , whereas it is 0 in all other cases. Let us decompose the theta series according to the ideal classes \(\mathfrak{K} \in J / P\) into partial Hecke theta series \[ \theta^ {p} (\mathfrak {K}, \chi , z) = \sum_ {a \in (\hat {\mathfrak {K}} \cap \hat {\mathcal {O}}) \cup \{0 \}} \chi (a) N (a ^ {p}) e ^ {\pi i \langle a z / | m d |, a \rangle}, \] where \(a\) varies over all ideal integers in the class \(\widehat{\mathfrak{K}}\in\widehat{K}^{*}/K^{*}\) which corresponds to the ideal class \(\mathfrak{K}\) under the isomorphism \(\widehat{K}^{*}/K^{*}\cong J/P\) . For these partial theta series, we want to deduce a transformation formula, and to this end we decompose them further into theta series for which we have the general transformation formula (3.6) at our disposal.

Lemma (7.6)

FC09-C07-U101 · Chapter VII, §7, source L20702 · not formalized

(7.6) Lemma. Assume that \(\mathfrak{m} \neq 1\) or \(p \neq 0\) . If \(x \bmod \mathfrak{m}\) varies over the classes of \((\mathcal{O} / \mathfrak{m})^*\) , then one has \[ \theta^ {p} (\mathfrak {K}, \chi , z) = \chi (a) N (a ^ {p}) \sum_ {x \bmod \mathfrak {m}} \chi (x) \theta_ {\Gamma} ^ {p} \bigl (x, 0, z | a ^ {2} / m d | \bigr), \] where \(\Gamma\) is the lattice \(\mathfrak{m} / \mathfrak{a} \subseteq \mathbf{R}\) and \[ \theta_ {\Gamma} ^ {p} (x, 0, z) = \sum_ {g \in \Gamma} N \big ((x + g) ^ {p} \big) e ^ {\pi i \langle (x + g) z, x + g \rangle}. \]

Convention / notation

FC09-C07-U102 · Chapter VII, §7, source L20732 · after FC09-C07-U045, FC09-C07-U099 · not formalized

For an admissible element \(p = (p_{\tau})\), write \(\overline{p}\) for the admissible element with components \(\overline{p}_{\tau} = p_{\overline{\tau}}\). From the transformation formula (3.6) for the series \(\theta_{\Gamma}^{p}\) and proposition (7.5) on Gauss sums, one obtains the transformation formula of theorem (7.7).

Theorem (7.7)

FC09-C07-U103 · Chapter VII, §7, source L20734 · not formalized

(7.7) Theorem. For a primitive character \(\chi\) of \((\widehat{\mathcal{O}}/\mathfrak{m})^{*}\) , one has the transformation formula \[ \theta^ {p} (\mathcal {K}, \chi , - 1 / z) = W (\chi , \overline {{p}}) N \big ((z / i) ^ {p + \frac {1}{2}} \big) \theta^ {\overline {{p}}} (\mathcal {K} ^ {\prime}, \overline {{\chi}}, z) \] with the constant factor \[ W (\chi , \overline {{p}}) = \left[ i ^ {T r (\overline {{p}})} N \left(\left(\frac {m d}{| m d |}\right) ^ {\overline {{p}}}\right) \right] ^ {- 1} \frac {\tau (\chi)}{\sqrt {\mathfrak {N} (\mathfrak {m})}}. \] This factor has absolute value \(|W(\chi, \overline{p})| = 1\) .

Definition / construction

FC09-C07-U104 · Chapter VII, §8, source L20888 · not formalized

Let \(\mathfrak{m}\) be again an integral ideal of the number field \(K\) and let \[ \chi : J ^ {\mathfrak {m}} \longrightarrow S ^ {1} \] be a character of the group of ideals relatively prime to m. With respect to this character, we form the L-series \[ L (\chi , s) = \sum_ {a} \frac {\chi (a)}{\mathfrak {N} (a) ^ {s}}, \] where a varies over the integral ideals of K and we put \(\chi(\mathfrak{a}) = 0\) whenever \((\mathfrak{a}, \mathfrak{m}) \neq 1\) . Then the following proposition holds in complete generality.

Not formalized. No checked compatible Lean owner supplies Neukirch’s Hecke-character parametrization and L-series equivalence with all continuity/conductor assertions in this row.

Proposition (8.1)

FC09-C07-U105 · Chapter VII, §8, source L20902 · not formalized

(8.1) Proposition. The L-series \(L(\chi, s)\) converges absolutely and uniformly in the domain \(\operatorname{Re}(s) \geq 1 + \delta\) , for all \(\delta > 0\) , and one has \[ L (\chi , s) = \prod_ {\mathfrak {p}} \frac {1}{1 - \chi (\mathfrak {p}) \mathfrak {N} (\mathfrak {p}) ^ {- s}}, \] where p varies over the prime ideals of K.

Not formalized. No checked compatible Lean owner supplies Neukirch’s Hecke-character parametrization and L-series equivalence with all continuity/conductor assertions in this row.

Definition / construction

FC09-C07-U106 · Chapter VII, §8, source L20998 · after FC09-C07-U103 · not formalized

The L-series of a Größencharacter of \(J^{m}\) is called a Hecke L-series. If \(\chi\) is a (generalized) Dirichlet character mod m, i.e., a character of the ray class group \(J^{m}/P^{m}\) , then we call it a (generalized) Dirichlet L-series. The proof of the functional equation of the Hecke L-series proceeds in exactly the same way as for the Dedekind zeta function, except that it is based on the theta transformation formula (7.7).

Not formalized. No checked compatible Lean owner supplies Neukirch’s Hecke-character parametrization and L-series equivalence with all continuity/conductor assertions in this row.

Convention / notation

FC09-C07-U107 · Chapter VII, §8, source L21032 · after FC09-C07-U078 · not formalized

The character \(\chi_{\infty}\) of \(R^{*}\) corresponding to \(\chi\) is given by (6.7) as \[ \chi_ {\infty} (x) = N \left(x ^ {p} | x | ^ {- p + i q}\right), \] for an admissible \(p \in \prod_{\tau} \mathbb{Z}\) and a \(q \in \mathbf{R}_{\pm}\) . We put \(\mathbf{s} = s\mathbf{1} + p - iq\) , where \(s \in \mathbb{C}\) is a single complex variable, and \[ L _ {\infty} (\chi , s) = L _ {X} (\mathbf {s}) = L _ {X} (s \mathbf {1} + p - i q). \]

Not formalized. No checked compatible Lean owner supplies Neukirch’s Hecke-character parametrization and L-series equivalence with all continuity/conductor assertions in this row.

Proposition (8.3)

FC09-C07-U108 · Chapter VII, §8, source L21164 · not formalized

(8.3) Proposition. The function \[ \Lambda (\mathfrak {K}, \chi , s) = \left(| d _ {K} | \mathfrak {N} (\mathfrak {m})\right) ^ {s / 2} L _ {\infty} (\chi , s) L (\mathfrak {K}, \chi , s) \] is the Mellin transform \[ \varLambda (\mathfrak {K}, \chi , s) = L (f, s ^ {\prime}) \] of the function \[ f (t) = f _ {F} (\mathfrak {K}, \chi , t) = \frac {c (\chi)}{w} \int_ {F} N (x ^ {(p - i q) / 2}) \theta (\mathfrak {K}, \chi , i x t ^ {1 / n}) d ^ {*} x \] at \(s' = \frac{1}{2}(s + Tr(p - iq) / n)\) . Here we have set \(n = [K : \mathbb{Q}]\) , \(c(\chi) = N(|md|^{-p + iq})^{1/2}\) , and \(w\) denotes the number of roots of unity in \(K\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s Hecke-character parametrization and L-series equivalence with all continuity/conductor assertions in this row.

Proposition (8.4)

FC09-C07-U109 · Chapter VII, §8, source L21236 · not formalized

(8.4) Proposition. We have \(f_{F}(\mathfrak{K},\chi ,t) = a_{0} + O(e^{-ct^{1 / n}})\) for some \(c > 0\) , and \[ a _ {0} = \frac {N (| d | ^ {i q / 2})}{w} \int_ {F} N (x ^ {- i q / 2}) d ^ {*} x \] if \(\mathfrak{m} = 1\) and \(p = 0\) , and \(a_0 = 0\) otherwise. Furthermore we have \[ f _ {F} \Big (\mathfrak {K}, \chi , \frac {1}{t} \Big) = W (\chi) t ^ {\frac {1}{2} + T r (p) / n} f _ {F ^ {- 1}} (\mathfrak {K} ^ {\prime}, \overline {{\chi}}, t) \] where \(\mathfrak{K}\mathfrak{K}' = [\mathfrak{m}\mathfrak{d}]\) , and the constant factor is given by \[ W (\chi) = \left[ i ^ {T r (\overline {{p}})} N \left(\left(\frac {m d}{| m d |}\right) ^ {\overline {{p}}}\right) \right] ^ {- 1} \frac {\tau (\chi_ {\mathrm{f}})}{\sqrt {\mathfrak {N} (\mathfrak {m})}}. \]

Not formalized. No checked compatible Lean owner supplies Neukirch’s Hecke-character parametrization and L-series equivalence with all continuity/conductor assertions in this row.

Theorem (8.5)

FC09-C07-U110 · Chapter VII, §8, source L21274 · not formalized

(8.5) Theorem. Let \(\chi\) be a primitive Größencharacter mod \(\mathfrak{m}\) . Then the function \[ \varLambda (\mathfrak {K}, \chi , s) = \left(| d _ {K} | \mathfrak {N} (\mathfrak {m})\right) ^ {s / 2} L _ {\infty} (\chi , s) L (\mathfrak {K}, \chi , s), \quad \mathrm{Re} (s) > 1, \] has a meromorphic continuation to the complex plane \(\mathbb{C}\) and satisfies the functional equation \[ \Lambda (\mathfrak {K}, \chi , s) = W (\chi) \Lambda (\mathfrak {K} ^ {\prime}, \overline {{{{\chi}}}}, 1 - s) \] where \(\mathfrak{K}\mathfrak{K}' = [\mathfrak{m}\mathfrak{d}]\) , and the constant factor is given by \[ W (\chi) = \left[ i ^ {T r (\overline {{p}})} N \left(\left(\frac {m d}{| m d |}\right) ^ {\overline {{p}}}\right) \right] ^ {- 1} \frac {\tau (\chi_ {\mathrm{f}})}{\sqrt {\mathfrak {N} (\mathfrak {m})}}. \] It has absolute value \(|W(\chi)| = 1\) . \(\Lambda(\mathfrak{K},\chi,s)\) is holomorphic except for poles of order at most one at \(s=Tr(-p+iq)/n\) and \(s=1+Tr(p+iq)/n\) . In the case \(m\neq1\) or \(p\neq0\) , \(\Lambda(\mathfrak{K},\chi,s)\) is holomorphic on all of C.

Not formalized. No checked compatible Lean owner supplies Neukirch’s Hecke-character parametrization and L-series equivalence with all continuity/conductor assertions in this row.

Corollary (8.6)

FC09-C07-U111 · Chapter VII, §8, source L21320 · not formalized

(8.6) Corollary. The \(L\) -series \(\Lambda(\chi, s)\) admits a holomorphic continuation to \[ \mathbb {C} \setminus \left\{T r (- p + i q) / n, 1 + T r (p + i q) / n \right\} \] and satisfies the functional equation \[ \Lambda (\chi , s) = W (\chi) \Lambda (\overline {{{{\chi}}}}, 1 - s). \] It is holomorphic on all of \(\mathbb{C}\) , if \(\mathfrak{m} \neq 1\) or \(p \neq 0\) .

Not formalized. No checked compatible Lean owner supplies Neukirch’s Hecke-character parametrization and L-series equivalence with all continuity/conductor assertions in this row.

Definition / construction

FC09-C07-U112 · Chapter VII, §9, source L21346 · not formalized

We first prove a new kind of unit theorem for which we need the following notions from linear algebra. Let V be an n-dimensional R-vector space, k a subfield of R, and \(V_{k}\) a fixed k-structure of V, i.e., a k-subspace such that \(V = V_{k} \otimes_{k} R\) . By definition, an (open) k-rational simplicial cone of dimension d is a subset of the form \[ C \left(v _ {1}, \dots , v _ {d}\right) = \left\{t _ {1} v _ {1} + \dots + t _ {d} v _ {d} \mid t _ {\ell} \in \mathbb {R} _ {+} ^ {*} \right\} \] where \(v_{1}, \ldots, v_{d}\) are linearly independent vectors in \(V_{k}\) . A finite disjoint union of k-rational simplicial cones is called a k-rational polyhedric cone. We call a linear form L on V k-rational if its coefficients with respect to a k-basis of \(V_{k}\) lie in k.

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Lemma (9.1)

FC09-C07-U113 · Chapter VII, §9, source L21354 · not formalized

(9.1) Lemma. Every nonempty subset different from \(\{0\}\) of the form \[ P = \left\{x \in V \mid L _ {i} (x) \geq 0, \quad 0 < i \leq \ell , M _ {j} (x) > 0, 0 < j \leq m \right\} \] with nonzero k-rational linear forms \(L_{i}\) , \(M_{j}\) ( \(\ell = 0\) or m = 0 is allowed) is a disjoint union of finitely many k-rational cones, and possibly the origin.

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Corollary (9.2)

FC09-C07-U114 · Chapter VII, §9, source L21390 · not formalized

(9.2) Corollary. If \(C\) and \(C'\) are \(k\) -rational polyhedric cones, then \(C \setminus C'\) is also a \(k\) -rational polyhedric cone.

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Convention / notation

FC09-C07-U115 · Chapter VII, §9, source L21412 · not formalized

Let \(K\) be a number field of degree \(n = [K : \mathbb{Q}]\) , and let \(\mathbf{R} = \left[\prod_{\tau} \mathbb{C}\right]^+\) be the corresponding Minkowski space \((\tau \in \operatorname{Hom}(K, \mathbb{C}))\) . Define \[ \mathbf {R} _ {(+)} ^ {*} = \left\{\left(x _ {\tau}\right) \in \mathbf {R} ^ {*} \mid x _ {\tau} > 0 \text { for all real } \tau \right\}. \] (Observe that one has \(\mathbf{R}_{(+)}^{*} = \mathbf{R}_{+}^{*}\) only in the case where \(K\) is totally real.) Since \(\mathbf{R} = K\otimes_{\mathbb{Q}}\mathbb{R}\) , the field \(K\) is a \(\mathbb{Q}\) -structure of \(\mathbf{R}\) . The group \[ \mathcal {O} _ {+} ^ {*} = \mathcal {O} ^ {*} \cap \mathbf {R} _ {(+)} ^ {*} \] of totally positive units acts on \(\mathbf{R}_{(+)}^{*}\) via multiplication, and we will show that this action has a fundamental domain which is a Q-rational polyhedric cone:

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Shintani’s Unit Theorem (9.3)

FC09-C07-U116 · Chapter VII, §9, source L21426 · not formalized

(9.3) Shintani’s Unit Theorem. If \(E\) is a subgroup of finite index in \(\mathcal{O}_+^*\) , then there exists a \(\mathbb{Q}\) -rational polyhedric cone \(P\) such that \[ \mathbf {R} _ {(+)} ^ {*} = \bigcup_ {\varepsilon \in E} \varepsilon P \quad (d i s j o i n t u n i o n). \]

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Lemma (9.4)

FC09-C07-U117 · Chapter VII, §9, source L21532 · not formalized

(9.4) Lemma. There is a bijection \[ (1 + \mathfrak {a} ^ {- 1} \mathfrak {m}) _ {+} / E \stackrel {{\sim}} {{\longrightarrow}} \mathfrak {K} _ {\text { int }}, \quad \bar {a} \longmapsto a \mathfrak {a}, \] onto the set \(\mathcal{K}_{\mathrm{int}}\) of integral ideals in \(\mathcal{K}\) .

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Proposition (9.5)

FC09-C07-U118 · Chapter VII, §9, source L21574 · not formalized

(9.5) Proposition. The sets \(R(\mathfrak{K}, C_i)\) are finite, and one has \[ \zeta (\mathfrak {K}, s) = \frac {1}{\mathfrak {N} (\mathfrak {a}) ^ {s}} \sum_ {i = 1} ^ {m} \sum_ {x \in R (\mathfrak {K}, C _ {i})} \zeta (C _ {i}, x, s) \] with the zeta functions \[ \zeta (C _ {i}, x, s) = \sum_ {\mathbf {z}} \left| N (x + z _ {1} v _ {i 1} + \dots + z _ {d _ {i}} v _ {i d _ {i}}) \right| ^ {- s}, \] where \(\mathbf{z} = (z_{1},\dots ,z_{d_{i}})\) varies over all \(d_{i}\) -tuples of nonnegative integers.

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Corollary (9.6)

FC09-C07-U119 · Chapter VII, §9, source L21618 · not formalized

(9.6) Corollary. For the Dirichlet \(L\) -series attached to the Dirichlet character \(\chi : J^{\mathfrak{m}} / P^{\mathfrak{m}} \to \mathbb{C}^{*}\) , we have the decomposition \[ L (\chi , s) = \sum_ {\mathfrak {K}} \frac {\chi (\mathfrak {a})}{\mathfrak {N} (\mathfrak {a}) ^ {s}} \sum_ {i = 1} ^ {m} \sum_ {x \in R (\mathfrak {K}, C _ {i})} \zeta (C _ {i}, x, s), \] where \(\mathfrak{K}\) runs through the classes \(J^{\mathfrak{m}} / P^{\mathfrak{m}}\) , and \(\mathfrak{a}\) denotes an integral ideal in \(\mathfrak{K}\) , one for each class.

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Definition / construction

FC09-C07-U120 · Chapter VII, §9, source L21628 · not formalized

Let \(A\) be a real \(r \times n\) -matrix, \(r \leq n\) , with positive entries \(a_{ji}\) , \(1 \leq j \leq r\) , \(1 \leq i \leq n\) . From this matrix we construct the linear forms \[ L _ {j} (t _ {1}, \dots , t _ {n}) = \sum_ {i = 1} ^ {n} a _ {j i} t _ {i} \quad \text { and } \quad L _ {i} ^ {*} (z _ {1}, \dots , z _ {r}) = \sum_ {j = 1} ^ {r} a _ {j i} z _ {j}. \] For an \(r\) -tuple \(x = (x_1, \ldots, x_r)\) of positive real numbers, we write the following series \[ \zeta (A, x, s) = \sum_ {z _ {1}, \dots , z _ {r} = 0} ^ {\infty} \prod_ {i = 1} ^ {n} L _ {i} ^ {*} (z + x) ^ {- s}. \] On the other hand we define the generalized Bernoulli polynomials \(B_{k}(A,x)\) by \[ B _ {k} (A, x) = \frac {1}{n} \sum_ {i = 1} ^ {n} B _ {k} (A, x) ^ {(i)}, \] where \(B_{k}(A,x)^{(i)} / (k!)^{n}\) is the coefficient of \[ u ^ {(k - 1) n} (t _ {1} \dots t _ {i - 1} t _ {i + 1} \dots t _ {n}) ^ {k - 1} \] in the Laurent expansion at 0 of the function \[ \prod_ {j = 1} ^ {r} \left. \frac {\exp (u x _ {j} L _ {j} (t))}{\exp (u L _ {j} (t)) - 1} \right| _ {t _ {i} = 1} \] in the variables \(u, t_1, \ldots, t_{i-1}, t_{i+1}, \ldots, t_n\) . For \(r = n = 1\) and \(A = a\) , we have \(B_k(a, x) = a^{k-1}B_k(x)\) , with the usual Bernoulli polynomial \(B_k(x)\) (see §1, exercise 2). The equation \[ B _ {k} (A, 1 - x) = (- 1) ^ {n (k - 1) + r} B _ {k} (A, x), \] where \(1 - x\) signifies \((1 - x_{1},\ldots ,1 - x_{r})\) , is easily proved.

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Proposition (9.7)

FC09-C07-U121 · Chapter VII, §9, source L21666 · not formalized

(9.7) Proposition. The series \(\zeta(A, x, s)\) is absolutely convergent for \(\operatorname{Re}(s) > r/n\) , and it can be meromorphically continued to the whole complex plane. Its values at the points \(s = 1 - k\) , \(k = 1, 2, \ldots\) , are given by \[ \zeta (A, x, 1 - k) = (- 1) ^ {r} \frac {B _ {k} (A , x)}{k ^ {n}}. \]

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Theorem (9.8)

FC09-C07-U122 · Chapter VII, §9, source L21798 · not formalized

(9.8) Theorem. The values of the partial zeta function \(\zeta(\mathfrak{K}, s)\) at the integral points \(s = 1 - k\) , \(k = 1, 2, 3, \ldots\) , are given by \[ \zeta (\mathfrak {K}, 1 - k) = \mathfrak {N} (\mathfrak {a}) ^ {k - 1} \sum_ {i = 1} ^ {m} \left[ (- 1) ^ {d _ {i}} \sum_ {x \in R (\mathfrak {K}, C _ {i})} \frac {B _ {k} (A _ {i} , x)}{k ^ {n}} \right], \] and the values of the Dirichlet \(L\) -series \(L(\chi, s)\) are given by \[ L (\chi , 1 - k) = \sum_ {\mathfrak {K}} \chi (\mathfrak {a}) \mathfrak {N} (\mathfrak {a}) ^ {k - 1} \sum_ {i = 1} ^ {m} \left[ (- 1) ^ {d _ {i}} \sum_ {x \in R (\mathfrak {K}, C _ {i})} \frac {B _ {k} (A _ {i} , x)}{k ^ {n}} \right]. \] Here \(\mathfrak{a}\) is an integral ideal in the class \(\mathfrak{K}\) of \(J^{\mathfrak{m}} / P^{\mathfrak{m}}\) .

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Corollary (9.9)

FC09-C07-U123 · Chapter VII, §9, source L21820 · not formalized

(9.9) Corollary (SIEGEL-KLINGEN). The values of the partial zeta function \(\zeta(\mathcal{R}, s)\) at the points \(s = 0, -1, -2, \ldots\) are rational numbers.

Not formalized. No checked compatible Lean owner supplies the Shintani cone decomposition / partial zeta special-value machinery required by this row.

Definition (10.1)

FC09-C07-U124 · Chapter VII, §10, source L21912 · not formalized

(10.1) Definition. Let \(L|K\) be a Galois extension of algebraic number fields with Galois group \(G\) , and let \((\rho, V)\) be a representation of \(G\) . Then the Artin \(L\) -series attached to \(\rho\) is defined to be \[ \mathcal {L} (L | K, \rho , s) = \prod_ {\mathfrak {p}} \frac {1}{\det (1 - \varphi_ {\mathfrak {P}} \mathfrak {N} (\mathfrak {p}) ^ {- s} ; V ^ {I _ {\mathfrak {P}}})}, \] where \(\mathfrak{p}\) runs through all prime ideals of \(K\) .

Not formalized. Pinned Mathlib has Maschke semisimplicity, representation characters and induction infrastructure, but this full finite-group character-theory or Artin-L bundle is not exported by the checked interfaces.

Definition / construction

FC09-C07-U125 · Chapter VII, §10, source L21936 · not formalized

The degree of a representation \((\rho, V)\) of a finite group G is the dimension of V. The representation is called irreducible if the G-module V does not admit any proper G-invariant subspace. An irreducible representation of an abelian group is simply a character \[ \rho : G \longrightarrow \mathbb {C} ^ {*} = G L _ {1} (\mathbb {C}). \] Two representations \((\rho, V)\) and \((\rho', V')\) are called equivalent if the G-modules V and \(V'\) are isomorphic. Every representation \((\rho, V)\) factors into a direct sum \[ V = V _ {1} \oplus \dots \oplus V _ {s} \] of irreducible representations. If an irreducible representation \((\rho_{\alpha}, V_{\alpha})\) is equivalent to precisely \(r_{\alpha}\) among the representations in this decomposition, then \(r_{\alpha}\) is called the multiplicity of \(\rho_{\alpha}\) in \(\rho\) , and one writes \[ \rho \sim \sum_ {\alpha} r _ {\alpha} \rho_ {\alpha}, \] where \(\rho_{\alpha}\) varies over all non-equivalent irreducible representations of G.

Definition / construction

FC09-C07-U126 · Chapter VII, §10, source L21956 · in Mathlib

The character of a representation \((\rho, V)\) is by definition the function \[ \chi_ {\rho}: G \longrightarrow \mathbb {C}, \quad \chi_ {\rho} (\sigma) = \operatorname{trace} \rho (\sigma). \]

Formalized. Mathlib/RepresentationTheory/Character.lean::namespace FDRep, def character — The representation character is defined pointwise as the linear trace of ρ(g), exactly Definition 10.2.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C07-U127 · Chapter VII, §10, source L21962 · not formalized

One has \(\chi_{\rho}(1)=\dim V=\operatorname{degree}(\rho)\) , and \(\chi_{\rho}(\sigma\tau\sigma^{-1})=\chi_{\rho}(\tau)\) for all \(\sigma,\tau\in G\) . In general, a function \(f:G\to C\) with the property that \(f(\sigma\tau\sigma^{-1})=f(\tau)\) is called a central function (or class function). The special importance of characters comes from the following fact: Two representations are equivalent if and only if their characters are equal. If \(\rho \sim \sum_{\alpha} r_{\alpha} \rho_{\alpha}\) , then \[ \chi_ {\rho} = \sum_ {\alpha} r _ {\alpha} \chi_ {\rho_ {\alpha}}. \]

Convention / notation

FC09-C07-U128 · Chapter VII, §10, source L21970 · not formalized

The character of the trivial representation \(\rho: G \to GL(V)\) , \(\dim V = 1\) , \(\rho(\sigma) = 1\) for all \(\sigma \in G\) , is the constant function of value 1, and is denoted by \(1_{G}\) , or simply 1. The regular representation is given by the G-module \[ V = \mathbb {C} [ G ] = \left\{\sum_ {\tau \in G} x _ {\tau} \tau \mid x _ {\tau} \in \mathbb {C} \right\}, \] on which the \(\sigma\in G\) act via multiplication on the left. It decomposes into the direct sum of the trivial representation \(V_{0}=\mathbb{C}\sum_{\sigma\in G}\sigma\) , and the augmentation representation \(\left\{\sum_{\sigma\in G}x_{\sigma}\sigma\mid\sum_{\sigma}x_{\sigma}=0\right\}\) . The character associated with the regular, resp. the augmentation representation, is denoted by \(r_{G}\) , resp. \(u_{G}\) . We thus have \(r_{G}=u_{G}+1_{G}\) , and explicitly: \(r_{G}(\sigma)=0\) for \(\sigma\neq1\) , \(r_{G}(1)=g=\#G\) .

Definition / construction

FC09-C07-U129 · Chapter VII, §10, source L21978 · not formalized

A character \(\chi\) is called irreducible if it belongs to an irreducible representation. Every central function \(\varphi\) can be written uniquely as a linear combination \[ \varphi = \sum c _ {\chi} \chi , \quad c _ {\chi} \in \mathbb {C}, \] of irreducible characters. \(\varphi\) is a character of a representation of G if and only if the \(c_{\chi}\) are rational integers \(\geq 0\) . For instance, for the character \(r_{G}\) of the regular representation we find \[ r _ {G} = \sum \chi (1) \chi , \] where \(\chi\) varies over all irreducible characters of G. Given any two central functions \(\varphi\) and \(\psi\) of G, we put \[ (\varphi , \psi) = \frac {1}{g} \sum_ {\sigma \in G} \varphi (\sigma) \overline {{\psi}} (\sigma), \quad g = \# G, \] where \(\overline{\psi}\) is the function which is the complex conjugate of \(\psi\) . For two irreducible characters \(\chi\) and \(\chi'\) , this gives \[ (\chi,\chi') = \begin{cases} 1, & \chi = \chi', \\ 0, & \chi \neq \chi', \end{cases} \] so the irreducible characters are orthonormal.

Frobenius Reciprocity (10.2)

FC09-C07-U130 · Chapter VII, §10, source L22024 · not formalized

(10.2) Frobenius Reciprocity. For every central function \(\psi\) on H there is one and only one central function \(h_{*}(\psi)\) on G such that one has \[ \left(\varphi , h _ {*} (\psi)\right) = \left(h ^ {*} (\varphi), \psi\right) \] for all central functions \(\varphi\) on \(G\) .

Convention / notation

FC09-C07-U131 · Chapter VII, §10, source L22034 · not formalized

\(H\) is a subgroup of \(G\) and \(h\) is inclusion. In this case we write \(\varphi|H\) or simply \(\varphi\) instead of \(h^{*}(\varphi)\) , and \(\psi_{*}\) instead of \(h_{*}(\psi)\) (the induced function). If \(\varphi\) is the character of a representation \((\rho,V)\) of G, then \(\varphi|H\) is the character of the representation \((\rho|H,V)\) . If \(\psi\) is the character of a representation \((\rho,V)\) of H, then \(\psi_{*}\) is the character of the representation \((\operatorname{ind}(\rho),\operatorname{Ind}_{G}^{H}(V))\) given by the induced G-module \[ \operatorname{Ind} _ {G} ^ {H} (V) = \left\{f: G \to V \mid f (\tau x) = \tau f (x) \quad \text {for all} \tau \in H \right\} \] on which \(\sigma \in G\) acts by \((\sigma f)(x) = f(x\sigma)\) (see chap. IV, §7). One has \[ \psi_ {*} (\sigma) = \sum_ {\tau} \psi (\tau \sigma \tau^ {- 1}), \] where \(\tau\) varies over a system of representatives on the right of G/H, and we put \(\psi(\tau\sigma\tau^{-1})=0\) if \(\tau\sigma\tau^{-1}\notin H\) . b) \(G\) is a quotient group \(H / N\) of \(H\) and \(h\) is the projection. We then write \(\varphi\) instead of \(h^{*}(\varphi)\) , and \(\psi_{\natural}\) instead of \(h_{*}(\psi)\) . One has \[ \psi_ {\natural} (\sigma) = \frac {1}{\# N} \sum_ {\tau \mapsto \sigma} \psi (\tau). \] If \(\varphi\) is the character of a representation \((\rho, V)\) of G, then \(h^{*}(\varphi)\) is the character of the representation \((\rho \circ h, V)\) .

Brauer’s Theorem (10.3)

FC09-C07-U132 · Chapter VII, §10, source L22062 · not formalized

(10.3) Brauer’s Theorem. Every character \(\chi\) of a finite group \(G\) is a \(\mathbb{Z}\) -linear combination of characters \(\chi_{i*}\) induced from characters \(\chi_i\) of degree 1 associated to subgroups \(H_i\) of \(G\) .

Proposition (10.4)

FC09-C07-U133 · Chapter VII, §10, source L22074 · not formalized

(10.4) Proposition. (i) For the principal character \(\chi = 1\) , one has \[ \mathcal {L} (L | K, \mathbf {1}, s) = \zeta_ {K} (s). \] (ii) If \(\chi, \chi'\) are two characters of \(G(L|K)\) , then \[ \mathcal {L} (L | K, \chi + \chi^ {\prime}, s) = \mathcal {L} (L | K, \chi , s) \mathcal {L} (L | K, \chi^ {\prime}, s). \] (iii) For a bigger Galois extension \(L' | K, L' \supseteq L \supseteq K\) , and a character \(\chi\) of \(G(L|K)\) one has \[ \mathcal {L} (L ^ {\prime} | K, \chi , s) = \mathcal {L} (L | K, \chi , s). \] (iv) If \(M\) is an intermediate field, \(L \supseteq M \supseteq K\) , and \(\chi\) is a character of \(G(L|M)\) , then \[ \mathcal {L} (L | M, \chi , s) = \mathcal {L} (L | K, \chi_ {*}, s). \]

Corollary (10.5)

FC09-C07-U134 · Chapter VII, §10, source L22184 · not formalized

(10.5) Corollary. One has \[ \zeta_ {L} (s) = \zeta_ {K} (s) \prod_ {\chi \neq \mathbf {1}} \mathcal {L} (L | K, \chi , s) ^ {\chi (1)}, \] where \(\chi\) varies over the nontrivial irreducible characters of \(G(L|K)\) .

Definition / construction

FC09-C07-U135 · Chapter VII, §10, source L22220 · not formalized

Composing with the Artin symbol \(\left(\frac{L|K}{\cdot}\right)\) , this gives a character of the ray class group \(J^{\dagger}/P^{\dagger}\) , i.e., a Dirichlet character mod f. It induces a character on \(J^{\dagger}\) , which we denote by \[ \widetilde {\chi}: J ^ {\mathfrak {f}} \to \mathbb {C} ^ {*}. \]

Theorem (10.6)

FC09-C07-U136 · Chapter VII, §10, source L22228 · not formalized

(10.6) Theorem. Let \(L|K\) be an abelian extension, let \(\mathfrak{f}\) be the conductor of \(L|K\) , let \(\chi \neq 1\) be an irreducible character of \(G(L|K)\) , and \(\widetilde{\chi}\) the associated Größencharakter mod \(\mathfrak{f}\) . Then the Artin L-series for the character \(\chi\) and the Hecke L-series for the Größencharakter \(\widetilde{\chi}\) satisfy the identity \[ \mathcal {L} (L | K, \chi , s) = \prod_ {\mathfrak {p} \in S} \frac {1}{1 - \chi (\varphi_ {\mathfrak {P}}) \mathfrak {N} (\mathfrak {p}) ^ {- s}} L (\widetilde {\chi}, s), \] where \(S = \{\mathfrak{p}|\mathfrak{f}|\chi (I_{\mathfrak{P}}) = 1\}\) .

Definition / construction

FC09-C07-U137 · Chapter VII, §11, source L22284 · not formalized

The discriminant \(\partial = \partial_{L|K}\) of a Galois extension \(L|K\) of algebraic number fields admits a fine structure based on group theory. It is expressed by a product decomposition \[ \mathfrak {d} = \prod f (\chi) ^ {\chi (1)}, \] where \(\chi\) varies over the irreducible characters of the Galois group \(G = G(L|K)\) . The ideals \(\mathfrak{f}(\chi)\) are given by \[ \mathfrak {f} (\chi) = \prod_ {\mathfrak {p} \nmid \infty} \mathfrak {p} ^ {f _ {\mathfrak {p}} (\chi)} \] with \[ f _ {\mathfrak {p}} (\chi) = \sum_ {i \geq 0} \frac {g _ {i}}{g _ {0}} \operatorname{codim} V ^ {G _ {i}}, \] where V is a representation with character \(\chi\) , \(G_{i}\) is the i-th ramification group of \(L_{P}|K_{p}\) , and \(g_{i}\) denotes its order. This discovery goes back to EMIL ARTIN and HELMUT HASSE. The ideals \(f(\chi)\) are called Artin conductors. They play an important rôle in the functional equation of the Artin L-series, which we are going to prove in the next section. Here we collect the properties needed for this, following essentially the treatment given by J.-P.SERRE in [122].

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Definition / construction

FC09-C07-U138 · Chapter VII, §11, source L22316 · not formalized

One has \(i_G(\tau \sigma \tau^{-1}) = i_G(\sigma)\) , and \(i_H(\sigma) = i_G(\sigma)\) for every subgroup \(H \subseteq G\) . If \(L|K\) is unramified, then \(i_G(\sigma) = 0\) for all \(\sigma \in G\) , \(\sigma \neq 1\) . We put \[ a _ {G} (\sigma) = \left\{ \begin{array}{l l} - f i _ {G} (\sigma) & \mathrm{for} \sigma \neq 1, \\ f \sum_ {\tau \neq 1} i _ {G} (\tau) & \mathrm{for} \sigma = 1. \end{array} \right. \] \(a_{G}\) is a central function on \(G\) , and we have \[ (a _ {G}, \mathbf {1} _ {G}) = \frac {1}{\# G} \sum_ {\sigma \in G} a _ {G} (\sigma) = 0. \] We may therefore write \[ a _ {G} = \sum_ {\chi} f (\chi) \chi , \quad f (\chi) \in \mathbb {C}, \] with \(\chi\) varying over the irreducible characters of G. Our chief problem is to prove that the coefficients \(f(\chi)\) are rational integers \(\geq 0\) . Once we have shown this, we may form the ideal \(f_{\mathfrak{p}}(\chi) = \mathfrak{p}^{f(\chi)}\) , which will be the p-component of the global Artin conductor that we want. First we prove that the function \(a_{G}\) satisfies the following properties (we use the notation of the preceding section).

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Proposition (11.1)

FC09-C07-U139 · Chapter VII, §11, source L22336 · not formalized

(11.1) Proposition. (i) If \(H\) is a normal subgroup of \(G\) , then \[ a _ {G / H} = (a _ {G}) _ {\natural}. \] (ii) If \(H\) is any subgroup of \(G\) , and if \(K'\) is the fixed field with discriminant \(\mathfrak{d}_{K'|K} = \mathfrak{p}^{\nu}\) , then \[ a _ {G} | H = \nu r _ {H} + f _ {K ^ {\prime} | K} a _ {H}. \] (iii) Let \(G_{i}\) be the \(i\) -th ramification group of \(G\) , \(u_{i}\) the augmentation character of \(G_{i}\) , and \((u_{i})_{*}\) the character of \(G\) induced from \(u_{i}\) . Then one has \[ a _ {G} = \sum_ {i = 0} ^ {\infty} \frac {1}{\left(G _ {0} : G _ {i}\right)} \left(u _ {i}\right) _ {*}. \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Convention / notation

FC09-C07-U140 · Chapter VII, §11, source L22412 · not formalized

\(g = \# G\) . For any central function \(\varphi\) of \(G\) , we put \[ f (\varphi) = (\varphi , a _ {G}) \] and \[ \varphi (G _ {i}) = \frac {1}{g _ {i}} \sum_ {\sigma \in G _ {i}} \varphi (\sigma), \quad g _ {i} = \# G _ {i}. \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Proposition (11.2)

FC09-C07-U141 · Chapter VII, §11, source L22424 · not formalized

(11.2) Proposition. (i) If \(\varphi\) is a central function on the quotient group \(G / H\) , and \(\varphi'\) is the corresponding central function on \(G\) , then \[ f (\varphi) = f \left(\varphi^ {\prime}\right). \] (ii) If \(\varphi\) is a central function on a subgroup \(H\) of \(G\) , and \(\varphi_{*}\) is the central function induced by \(\varphi\) on \(G\) , then \[ f (\varphi_ {*}) = v _ {K} \left(\mathfrak {d} _ {K ^ {\prime} | K}\right) \varphi (1) + f _ {K ^ {\prime} | K} f (\varphi). \] (iii) For a central function \(\varphi\) on \(G\) , one has \[ f (\varphi) = \sum_ {i \geq 0} \frac {g _ {i}}{g _ {0}} (\varphi (1) - \varphi (G _ {i})). \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Proposition (11.3)

FC09-C07-U142 · Chapter VII, §11, source L22467 · not formalized

(11.3) Proposition. Let \(\chi\) be a character of \(G\) of degree 1. Let \(j\) be the biggest integer such that \(\chi|_{G_j} \neq \mathbf{1}_{G_j}\) (when \(\chi = \mathbf{1}_G\) we put \(j = -1\) ). Then we have \[ f (\chi) = \eta_ {L | K} (j) + 1, \] and this is a rational integer \(\geq 0\) .

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Theorem (11.4)

FC09-C07-U143 · Chapter VII, §11, source L22517 · not formalized

(11.4) Theorem. If \(\chi\) is a character of the Galois group \(G = G(L|K)\) , then \(f(\chi)\) is a rational integer \(\geq 0\) .

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Definition (11.5)

FC09-C07-U144 · Chapter VII, §11, source L22519 · not formalized

(11.5) Definition. We define the (local) Artin conductor of the character \(\chi\) of \(G = G(L|K)\) to be the ideal \[ \mathfrak {f} _ {\mathfrak {p}} (\chi) = \mathfrak {p} ^ {f (\chi)}. \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Proposition (11.6)

FC09-C07-U145 · Chapter VII, §11, source L22533 · not formalized

(11.6) Proposition. Let \(L|K\) be a Galois extension of local fields, and let \(\chi\) be a character of \(G(L|K)\) of degree 1. Let \(L_{\chi}\) be the fixed field of the kernel of \(\chi\) , and \(\{\) the conductor of \(L_{\chi}|K\) . Then one has \[ f = f _ {p} (\chi). \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Definition / construction

FC09-C07-U146 · Chapter VII, §11, source L22547 · after FC09-C07-U141 · not formalized

We now leave the local situation, and suppose that \(L|K\) is a Galois extension of global fields. Let \(\mathfrak{p}\) be a prime ideal of \(K\) , \(\mathfrak{P}| \mathfrak{p}\) a prime ideal of \(L\) lying above \(\mathfrak{p}\) . Let \(L_{\mathfrak{P}}|K_{\mathfrak{p}}\) be the completion of \(L|K\) , and \(G_{\mathfrak{P}} = G(L_{\mathfrak{P}}|K_{\mathfrak{p}})\) the decomposition group of \(\mathfrak{P}\) over \(K\) . We denote the function \(a_{G_{\mathfrak{P}}}\) on \(G_{\mathfrak{P}}\) by \(a_{\mathfrak{P}}\) , and extend it to \(G = G(L|K)\) by zero. The central function \[ a _ {\mathfrak {p}} = \sum_ {\mathfrak {P} | \mathfrak {p}} a _ {\mathfrak {P}} \] immediately turns out to be the function \((a_{\mathfrak{P}})_*\) induced by \(a_{\mathfrak{P}}|G_{\mathfrak{P}}\) . It is therefore the character of a representation of \(G\) . If now \(\chi\) is a character of \(G\) , then we put \[ f (\chi , \mathfrak {p}) = (\chi , a _ {\mathfrak {p}}) = f (\chi | G _ {\mathfrak {P}}). \] Then \(\mathfrak{f}_{\mathfrak{p}}(\chi) = \mathfrak{p}^{f(\chi, \mathfrak{p})}\) is the Artin conductor of the restriction of \(\chi\) to \(G_{\mathfrak{P}} = G(L_{\mathfrak{P}} | K_{\mathfrak{p}})\) . In particular, we have \(\mathfrak{f}_{\mathfrak{p}}(\chi) = 1\) if p is unramified. We define the (global) Artin conductor of \(\chi\) to be the product \[ f (\chi) = \prod_ {\mathfrak {p} \nmid \infty} f _ {\mathfrak {p}} (\chi). \] Whenever precision is called for, we write \(f(L|K,\chi)\) instead of \(f(\chi)\) . The properties (11.2) of the numbers \(f(\chi,\mathfrak{p})\) transfer immediately to the Artin conductor \(f(\chi)\) , and we obtain the proposition (11.7): \(f(\chi+\chi') = f(\chi)f(\chi')\) and \(f(1) = (1)\), and the conductor of a character of a Galois subextension \(L'|K\) is computed from that character on \(G(L'|K)\).

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Proposition (11.7)

FC09-C07-U147 · Chapter VII, §11, source L22567 · not formalized

(11.7) Proposition. (i) \(f(\chi + \chi') = f(\chi)f(\chi')\) , \(f(1) = (1)\) . (ii) If \(L' | K\) is a Galois subextension of \(L|K\) , and \(\chi\) is a character of \(G(L'|K)\) , then \[ \mathfrak {f} (L | K, \chi) = \mathfrak {f} (L ^ {\prime} | K, \chi). \] (iii) If \(H\) is a subgroup of \(G\) with fixed field \(K'\) , and if \(\chi\) is a character of \(H\) , then \[ \mathfrak {f} (L | K, \chi_ {*}) = \mathfrak {d} _ {K ^ {\prime} | K} ^ {\chi (1)} N _ {K ^ {\prime} | K} \left(\mathfrak {f} (L | K ^ {\prime}, \chi)\right). \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Convention / notation

FC09-C07-U148 · Chapter VII, §11, source L22625 · not formalized

Applying (iii) to \(\chi = \mathbf{1}_{H}\) and denoting the induced character \(\chi_{*}\) by \(s_{G/H}\), one has \(\mathfrak{f}(\chi) = 1\), and so corollary (11.8): \(\mathfrak{d}_{K'|K} = \mathfrak{f}(L|K, s_{G/H})\).

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Corollary (11.8)

FC09-C07-U149 · Chapter VII, §11, source L22627 · not formalized

(11.8) Corollary. \(\mathfrak{d}_{K'|K} = \mathfrak{f}(L|K,s_{G / H})\) .

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Convention / notation

FC09-C07-U150 · Chapter VII, §11, source L22629 · not formalized

If in particular \(H = \{1\}\) , then \(s_{G/H}\) is the character \(r_{G}\) of the regular representation. Its decomposition into irreducible characters \(\chi\) is given by \[ r _ {G} = \sum_ {\chi} \chi (1) \chi . \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Conductor-Discriminant-Formula (11.9)

FC09-C07-U151 · Chapter VII, §11, source L22637 · not formalized

(11.9) Conductor-Discriminant-Formula. For an arbitrary Galois extension \(L|K\) of global fields, one has \[ \mathfrak {d} _ {L | K} = \prod_ {\chi} f (\chi) ^ {\chi (1)}, \] where \(\chi\) varies over the irreducible characters of \(G(L|K)\) .

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Proposition (11.10)

FC09-C07-U152 · Chapter VII, §11, source L22653 · not formalized

(11.10) Proposition. Let \(L|K\) be a Galois extension of global fields, \(\chi\) a character of \(G(L|K)\) of degree 1, \(L_{\chi}\) the fixed field of the kernel of \(\chi\) , and \(\mathfrak{f}\) the conductor of \(L_{\chi}|K\) . Then one has \[ f = f (\chi). \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Definition / construction

FC09-C07-U153 · Chapter VII, §11, source L22659 · not formalized

Now let \(L|K\) be a Galois extension of algebraic number fields. We form the ideal \[ \mathfrak {c} (L | K, \chi) = \mathfrak {d} _ {K | \mathbb {Q}} ^ {\chi (1)} N _ {K | \mathbb {Q}} \big (\mathfrak {f} (L | K, \chi) \big) \] of Z. The positive generator of this ideal is the integer \[ c (L | K, \chi) = | d _ {K} | ^ {\chi (1)} \mathfrak {N} \big (\mathfrak {f} (L | K, \chi) \big). \]

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Proposition (11.11)

FC09-C07-U154 · Chapter VII, §11, source L22673 · not formalized

(11.11) Proposition. (i) \(c(L|K, \chi + \chi') = c(L|K, \chi)c(L|K, \chi')\) , \(c(L|K, 1) = |d_K|\) , (ii) \(c(L|K,\chi)=c(L'|K,\chi),\) (iii) \(c(L|K,\chi_{*}) = c(L|K^{\prime},\chi)\) .

Not formalized. No checked compatible Lean owner supplies Artin conductors, local conductor exponents, or the conductor-discriminant formulas required by this row.

Definition / construction

FC09-C07-U155 · Chapter VII, §12, source L22683 · not formalized

The first task is to complete the Artin \(L\) -series \[ \mathcal {L} (L | K, \chi , s) = \prod_ {\mathfrak {p} \nmid \infty} \frac {1}{\det \left(1 - \varphi_ {\mathfrak {P}} \mathfrak {N} (\mathfrak {p}) ^ {- s} ; V ^ {I _ {\mathfrak {P}}}\right)}, \] for the character \(\chi\) of \(G = G(L|K)\) , by the appropriate gamma factors. For every infinite place \(\mathfrak{p}\) of \(K\) we put \[ \mathcal {L} _ {\mathfrak {p}} (L | K, \chi , s) = \left\{ \begin{array}{l l} L _ {\mathbb {C}} (s) ^ {\chi (1)}, & \text { if } \mathfrak {p} \text { is complex }, \\ L _ {\mathbb {R}} (s) ^ {n ^ {+}} L _ {\mathbb {R}} (s + 1) ^ {n ^ {-}}, & \text { if } \mathfrak {p} \text { is real }, \end{array} \right. \] with the exponents \(n^{+} = \frac{\chi(1) + \chi(\varphi_{\mathfrak{P}})}{2}\) , \(n^{-} = \frac{\chi(1) - \chi(\varphi_{\mathfrak{P}})}{2}\) . Here \(\varphi_{\mathfrak{P}}\) is the distinguished generator of \(G(L_{\mathfrak{P}}|K_{\mathfrak{p}})\) , and \[ L _ {\mathbb {R}} (s) = \pi^ {- s / 2} \Gamma (s / 2), \quad L _ {\mathbb {C}} (s) = 2 (2 \pi) ^ {- s} \Gamma (s) \]

Not formalized. No checked compatible Lean owner supplies the Artin L-function functional equation, epsilon/root-number package, or Brauer-derived meromorphic continuation required by this row.

Proposition (12.1)

FC09-C07-U156 · Chapter VII, §12, source L22717 · not formalized

(12.1) Proposition. (i) \(\mathcal{L}_{\mathfrak{p}}(L|K,\chi +\chi ',s) = \mathcal{L}_{\mathfrak{p}}(L|K,\chi ,s)\mathcal{L}_{\mathfrak{p}}(L|K,\chi ',s).\) (ii) If \(L' | K\) is a Galois subextension of \(L | K\) and \(\chi\) a character of \(G(L' | K)\) , then \[ \mathcal {L} _ {\mathfrak {p}} (L | K, \chi , s) = \mathcal {L} _ {\mathfrak {p}} (L ^ {\prime} | K, \chi , s). \] (iii) If \(K'\) is an intermediate field of \(L|K\) and \(\chi\) a character of \(G(L|K')\) , then \[ \mathcal {L} _ {\mathfrak {p}} (L | K, \chi_ {*}, s) = \prod_ {\mathfrak {q} | \mathfrak {p}} \mathcal {L} _ {\mathfrak {q}} (L | K ^ {\prime}, \chi , s), \] where q varies over the places of \(K'\) lying above p.

Not formalized. No checked compatible Lean owner supplies the Artin L-function functional equation, epsilon/root-number package, or Brauer-derived meromorphic continuation required by this row.

Definition (12.2)

FC09-C07-U157 · Chapter VII, §12, source L22787 · not formalized

(12.2) Definition. The completed Artin \(L\) -series for the character \(\chi\) of \(G(L|K)\) is defined to be \[ \varLambda (L | K, \chi , s) = c (L | K, \chi) ^ {s / 2} \mathcal {L} _ {\infty} (L | K, \chi , s) \mathcal {L} (L | K, \chi , s), \] where \[ c (L | K, \chi) = | d _ {K} | ^ {\chi (1)} \mathfrak {N} \big (\mathfrak {f} (L | K, \chi) \big). \]

Not formalized. No checked compatible Lean owner supplies the Artin L-function functional equation, epsilon/root-number package, or Brauer-derived meromorphic continuation required by this row.

Proposition (12.3)

FC09-C07-U158 · Chapter VII, §12, source L22801 · not formalized

(12.3) Proposition. (i) \(\Lambda(L|K, \chi + \chi', s) = \Lambda(L|K, \chi, s)\Lambda(L|K, \chi', s)\) . (ii) If \(L' | K\) is a Galois subextension of \(L | K\) and \(\chi\) a character of \(G(L' | K)\) , then \[ \Lambda (L | K, \chi , s) = \Lambda (L ^ {\prime} | K, \chi , s). \] (iii) If \(K'\) is an intermediate field of \(L|K\) and \(\chi\) a character of \(G(L|K')\) , then \[ \varLambda (L | K, \chi_ {*}, s) = \varLambda (L | K ^ {\prime}, \chi , s). \]

Not formalized. No checked compatible Lean owner supplies the Artin L-function functional equation, epsilon/root-number package, or Brauer-derived meromorphic continuation required by this row.

Convention / notation

FC09-C07-U159 · Chapter VII, §12, source L22827 · after FC09-C07-U082 · not formalized

\(\chi\) becomes a Dirichlet character of conductor f, i.e., by (6.9), a primitive Größencharakter mod \(f(\chi)\) with exponent \(p = (p_{\tau})\) , so that \(p_{\tau} = 0\) if \(\tau\) is complex. This Größencharakter will be denoted \(\widetilde{\chi}\) . We put \(p_{\mathfrak{p}} = p_{\tau}\) if \(\mathfrak{p}\) is the place corresponding to the embedding \(\tau : K \to \mathbb{C}\) . The numbers \(p_{\mathfrak{p}}\) have the following Galois-theoretical meaning.

Not formalized. No checked compatible Lean owner supplies the Artin L-function functional equation, epsilon/root-number package, or Brauer-derived meromorphic continuation required by this row.

Lemma (12.4)

FC09-C07-U160 · Chapter VII, §12, source L22831 · not formalized

(12.4) Lemma. For every real place \(\mathfrak{p}\) of \(K\) one has \[ p _ {\mathfrak {p}} = \left[ L _ {\chi \mathfrak {P}}: K _ {\mathfrak {p}} \right] - 1. \]

Not formalized. No checked compatible Lean owner supplies the Artin L-function functional equation, epsilon/root-number package, or Brauer-derived meromorphic continuation required by this row.

Proposition (12.5)

FC09-C07-U161 · Chapter VII, §12, source L22863 · not formalized

(12.5) Proposition. The completed Artin L-series for the character \(\chi\) of degree 1 and the completed Hecke L-series for the Größencharakter \(\widetilde{\chi}\) coincide: \[ \Lambda (L | K, \chi , s) = \Lambda (\widetilde {\chi}, s). \]

Not formalized. No checked compatible Lean owner supplies the Artin L-function functional equation, epsilon/root-number package, or Brauer-derived meromorphic continuation required by this row.

Theorem (12.6)

FC09-C07-U162 · Chapter VII, §12, source L22939 · not formalized

(12.6) Theorem. The Artin L-series \(\Lambda(L|K,\chi,s)\) admits a meromorphic continuation to C and satisfies the functional equation \[ \Lambda (L | K, \chi , s) = W (\chi) \Lambda (L | K, \overline {{{{\chi}}}}, 1 - s) \] with a constant \(W(\chi)\) of absolute value 1.

Not formalized. No checked compatible Lean owner supplies the Artin L-function functional equation, epsilon/root-number package, or Brauer-derived meromorphic continuation required by this row.

Definition (13.1)

FC09-C07-U163 · Chapter VII, §13, source L23027 · in Mathlib

(13.1) Definition. Let M be a set of prime ideals of K. The limit \[ d (M) = \lim _ {s \rightarrow 1 + 0} \frac {\sum_ {\mathfrak {p} \in M} \mathfrak {N} (\mathfrak {p}) ^ {- s}}{\sum_ {\mathfrak {p}} \mathfrak {N} (\mathfrak {p}) ^ {- s}}, \] provided it exists, is called the Dirichlet density of M.

Formalized. Mathlib/NumberTheory/NumberField/DirichletDensity.lean::HasDirichletDensity, primeIdealZetaSum — Mathlib’s HasDirichletDensity is exactly the limit of the prime-ideal zeta sum over the chosen set divided by the corresponding sum over all prime ideals as s→1+, matching Definition 13.1.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C07-U164 · Chapter VII, §13, source L23047 · after FC09-C07-U065 · not formalized

We write \(f(s) \sim g(s)\) if \(f(s) - g(s)\) is an analytic function at s = 1. Then we have \[ \log \zeta_ {K} (s) \sim \sum_ {\mathfrak {p}} \frac {1}{\mathfrak {N} (\mathfrak {p}) ^ {s}} \sim \sum_ {\deg (\mathfrak {p}) = 1} \frac {1}{\mathfrak {N} (\mathfrak {p}) ^ {s}}, \] because the sum \(\sum_{\deg (\mathfrak{p})\geq 2}\mathfrak{N}(\mathfrak{p})^{-s}\) taken over all \(\mathfrak{p}\) of degree \(\geq 2\) is analytic at \(s = 1\) . Furthermore, by (5.11), (ii), we have \(\zeta_K(s)\sim \frac{1}{s - 1}\) , and so \[ \sum_ {\mathfrak {p}} \frac {1}{\mathfrak {N} (\mathfrak {p}) ^ {s}} \sim \log \frac {1}{s - 1}. \]

Not formalized. Pinned Mathlib has the definition of Dirichlet density and current/external developments have Frobenius-prime infrastructure, but this row requires a prime-density, Chebotarev, splitting, or Artin-L theorem not yet proved in a checked compatible source.

Theorem (13.2)

FC09-C07-U165 · Chapter VII, §13, source L23073 · not formalized

(13.2) Theorem. Let \(\mathfrak{m}\) be a module of \(K\) and \(H^{\mathfrak{m}}\) an ideal group such that \(J^{\mathfrak{m}} \supseteq H^{\mathfrak{m}} \supseteq P^{\mathfrak{m}}\) with index \(h_{\mathfrak{m}} = (J^{\mathfrak{m}}: H^{\mathfrak{m}})\) . For every class \(\mathfrak{K} \in J^{\mathfrak{m}} / H^{\mathfrak{m}}\) , the set \(P(\mathfrak{K})\) of prime ideals in \(\mathfrak{K}\) has density \[ d (P (\mathfrak {K})) = \frac {1}{h _ {\mathfrak {m}}} \cdot \]

Lemma (13.3)

FC09-C07-U166 · Chapter VII, §13, source L23083 · not formalized

(13.3) Lemma. Let \(\chi\) be a nontrivial (irreducible) character of \(J^{\mathfrak{m}} / P^{\mathfrak{m}}\) (i.e., a character of degree 1). Then the Hecke \(L\) -series \[ L (\chi , s) = \prod_ {\mathfrak {p}} \frac {1}{1 - \chi (\mathfrak {p}) \mathfrak {N} (\mathfrak {p}) ^ {- s}} \] \((\chi (\mathfrak{p}) = 0\) for \(\mathfrak{p}|\mathfrak{m})\) satisfies \[ L (\chi , 1) \neq 0. \]

Definition / construction

FC09-C07-U167 · Chapter VII, §13, source L23131 · not formalized

Relating the prime ideals p of a class of \(J^{m}/P^{m}\) , via the class field theory isomorphism \(J^{m}/P^{m} \cong G(L|K)\) , to the Frobenius automorphisms \(\varphi_{\mathfrak{p}} = \left(\frac{L|K}{\mathfrak{p}}\right)\) , gives us a Galois-theoretic interpretation of the Dirichlet density theorem. We now deduce a more general density theorem which is particularly important in that it concerns arbitrary Galois extensions (not necessarily abelian). For every \(\sigma \in G(L|K)\) , let us consider the set \[ P _ {L | K} (\sigma) \] of all unramified prime ideals \(\mathfrak{p}\) of \(K\) such that there exists a prime ideal \(\mathfrak{P}|\mathfrak{p}\) of \(L\) satisfying \[ \sigma = \left(\frac {L | K}{\mathfrak {P}}\right), \] where \(\left(\frac{L|K}{\mathfrak{P}}\right)\) is the Frobenius automorphism \(\varphi_{P}\) of P over K. It is clear that this set depends only on the conjugacy class \[ \langle \sigma \rangle = \left\{\tau \sigma \tau^ {- 1} \mid \tau \in G (L | K) \right\} \] of \(\sigma\) and that one has \(P_{L|K}(\sigma) \cap P_{L|K}(\tau) = \emptyset\) if \(\langle \sigma \rangle \neq \langle \tau \rangle\) . What is the density of the set \(P_{L|K}(\sigma)\) ? The answer to this question is given by the Čebotarev density theorem.

Theorem (13.4)

FC09-C07-U168 · Chapter VII, §13, source L23151 · not formalized

(13.4) Theorem. Let \(L|K\) be a Galois extension with group \(G\) . Then for every \(\sigma \in G\) , the set \(P_{L|K}(\sigma)\) has a density, and it is given by \[ d (P _ {L | K} (\sigma)) = \frac {\# \langle \sigma \rangle}{\# G}. \]

Convention / notation

FC09-C07-U169 · Chapter VII, §13, source L23201 · not formalized

Let \(L|K\) be a finite extension of algebraic number fields. We denote by \(P(L|K)\) the set of all unramified prime ideals \(\mathfrak{p}\) of K which admit in L a prime divisor \(\mathfrak{P}\) of degree 1 over K. So, if \(L|K\) is Galois, then \(P(L|K)\) is just the set of all prime ideals of K which split completely in L.

Lemma (13.5)

FC09-C07-U170 · Chapter VII, §13, source L23203 · not formalized

(13.5) Lemma. Let \(N|K\) be a Galois extension containing \(L\) , and let \(G = G(N|K)\) , \(H = G(N|L)\) . Then one has \[ P (L | K) = \bigcup_ {\langle \sigma \rangle \cap H \neq \emptyset} P _ {N | K} (\sigma) \quad (d i s j o i n t u n i o n). \]

Corollary (13.6)

FC09-C07-U171 · Chapter VII, §13, source L23211 · not formalized

(13.6) Corollary. If \(L|K\) is an extension of degree \(n\) , then the set \(P(L|K)\) has density \(d(P(L|K)) \geq \frac{1}{n}\) . Furthermore, one has \[ d (P (L | K)) = \frac {1}{n} \Longleftrightarrow L | K \text { is Galois. } \]

Corollary (13.7)

FC09-C07-U172 · Chapter VII, §13, source L23237 · not formalized

(13.7) Corollary. If almost all prime ideals split completely in the finite extension \(L|K\) , then \(L = K\) .

Corollary (13.8)

FC09-C07-U173 · Chapter VII, §13, source L23247 · not formalized

(13.8) Corollary. An extension \(L|K\) is Galois if and only if every prime ideal in \(P(L|K)\) splits completely in \(L\) .

Proposition (13.9)

FC09-C07-U174 · Chapter VII, §13, source L23257 · not formalized

(13.9) Proposition (M. BAUER). If \(L|K\) is Galois and \(M|K\) is an arbitrary finite extension, then \[ P (L | K) \dot {\supseteq} P (M | K) \iff L \subseteq M. \]

Corollary (13.10)

FC09-C07-U175 · Chapter VII, §13, source L23271 · not formalized

(13.10) Corollary. A Galois extension \(L|K\) is uniquely determined by the set \(P(L|K)\) of prime ideals which split completely in it.