The Chebotarev Density Theorem in Lean

1. Dirichlet density🔗

Throughout, K denotes a number field, \mathcal{O}_K its ring of integers, and \mathfrak{p} ranges over nonzero prime ideals of \mathcal{O}_K with absolute norm \Norm\mathfrak{p} = [\mathcal{O}_K : \mathfrak{p}].

Definition1.1
uses 0
Used by 5
Reverse dependency previews
Preview
Lemma 1.1.1
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

A set S of nonzero prime ideals of \mathcal{O}_K has Dirichlet density \delta \in \mathbb{R}, written \delta(S) = \delta, if \lim_{s \to 1^+} \frac{\displaystyle\sum_{\mathfrak{p} \in S} \Norm\mathfrak{p}^{-s}}{\displaystyle\sum_{\mathfrak{p}} \Norm\mathfrak{p}^{-s}} = \delta, where the denominator sum runs over all nonzero prime ideals of \mathcal{O}_K.

Lean code for Definition1.1●1 definition
  • defdefined in CebotarevDensity/Density.lean
    complete
    def Chebotarev.HasDirichletDensity.{u_1} {K : Type u_1} [Field K]
  [NumberField K] (S : Set (Ideal (NumberField.RingOfIntegers K)))
  (δ : ℝ) : Prop
    def Chebotarev.HasDirichletDensity.{u_1}
  {K : Type u_1} [Field K] [NumberField K]
  (S :
    Set
      (Ideal
        (NumberField.RingOfIntegers K)))
  (δ : ℝ) : Prop
    The Dirichlet density of a set `S` of prime ideals of `𝓞 K` is `δ` when the ratio of partial
sums tends to `δ` as `s ↓ 1`.

Sharifi 7.1.13: `δ(S) = lim_{s → 1⁺} (Σ_{𝔭 ∈ S} N𝔭^{-s}) / (Σ_𝔭 N𝔭^{-s})`.

The denominator is asymptotically \log\bigl(1/(s-1)\bigr) as s \downarrow 1 (Sharifi Prop. 7.1.12, p. 140); the lemmas below break out the analytic ingredients.

Lemma1.2
uses 0used by 1✓L∃∀N

The higher-power tail of the log-Euler-product \sum_{\mathfrak{p},\, k \ge 2} \frac{\Norm\mathfrak{p}^{-2s}}{1 - \Norm\mathfrak{p}^{-s}} is bounded on a right neighbourhood of s = 1.

Lean code for Lemma1.2●1 theorem
  • theoremdefined in CebotarevDensity/Density.lean
    complete
    theorem Chebotarev.primeIdealZetaHigherTail_bounded.{u_1} (K : Type u_1)
  [Field K] [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1),
      ∑' (𝔭 : { 𝔭 // 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ }),
          ↑(Ideal.absNorm ↑𝔭) ^ (-2 * s) /
            (1 - ↑(Ideal.absNorm ↑𝔭) ^ (-s)) ≤
        C
    theorem Chebotarev.primeIdealZetaHigherTail_bounded.{u_1}
  (K : Type u_1) [Field K]
  [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in
      nhdsWithin 1 (Set.Ioi 1),
      ∑' (𝔭 : { 𝔭 // 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ }),
          ↑(Ideal.absNorm ↑𝔭) ^ (-2 * s) /
            (1 -
              ↑(Ideal.absNorm ↑𝔭) ^
                (-s)) ≤
        C
    Sharifi 7.1.12 proof (p. 140), bounded tail step. The geometric higher-power tail `Σ_𝔭
N𝔭^{-2s}/(1 - N𝔭^{-s}) = Σ_{𝔭, k≥2} N𝔭^{-ks}` is bounded on a right neighbourhood of `s = 1` (in
fact on `Re s > 1/2`). It dominates the weighted Euler-product log-tail `Σ_{𝔭, k≥2} N𝔭^{-ks}/k`, so
bounding it suffices for the source's "`log ζ_K(s) ~ Σ_𝔭 N𝔭^{-s}`".
Lemma1.3
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 1.5
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Euler-product-log identity: \bigl|\log\zeta_K(s) - \sum_\mathfrak{p} \Norm\mathfrak{p}^{-s}\bigr| \le C on a right neighbourhood of 1.

Lemma 1.2

Lean code for Lemma1.3●1 theorem
  • theoremdefined in CebotarevDensity/Density.lean
    complete
    theorem Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded.{u_1}
  (K : Type u_1) [Field K] [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1),
      |Real.log (NumberField.dedekindZeta K ↑s).re -
            Chebotarev.primeIdealZetaSum Set.univ s| ≤
        C
    theorem Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded.{u_1}
  (K : Type u_1) [Field K]
  [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in
      nhdsWithin 1 (Set.Ioi 1),
      |Real.log
              (NumberField.dedekindZeta K
                  ↑s).re -
            Chebotarev.primeIdealZetaSum
              Set.univ s| ≤
        C
    Euler-product-log identity: `log ζ_K(s) = Σ_𝔭 N𝔭^{-s} + O(1)` as `s ↓ 1`
(Sharifi 7.1.12, p. 140).
Proof for Lemma 1.3
uses 1

We have \log\zeta_K(s) = \sum_\mathfrak{p} \Norm\mathfrak{p}^{-s} + \sum_{\mathfrak{p},\, k \ge 2} \Norm\mathfrak{p}^{-ks}/k; the tail is bounded by Lemma 1.2.

Lemma 1.2

Lemma1.4
uses 0
Used by 2
Reverse dependency previews
Preview
Lemma 1.5
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

Simple-pole identity: \bigl|\log\zeta_K(s) - \log(1/(s-1))\bigr| \le C on a right neighbourhood of 1.

Lean code for Lemma1.4●1 theorem
  • theoremdefined in CebotarevDensity/Density.lean
    complete
    theorem Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded.{u_1}
  (K : Type u_1) [Field K] [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1),
      |Real.log (NumberField.dedekindZeta K ↑s).re -
            Real.log (1 / (s - 1))| ≤
        C
    theorem Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded.{u_1}
  (K : Type u_1) [Field K]
  [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in
      nhdsWithin 1 (Set.Ioi 1),
      |Real.log
              (NumberField.dedekindZeta K
                  ↑s).re -
            Real.log (1 / (s - 1))| ≤
        C
    Sharifi 7.1.12 proof (p. 140), simple-pole identity: `log ζ_K(s) = log(1/(s-1)) + O(1)` as
`s ↓ 1`, from the simple pole of `ζ_K` at `s=1` (mathlib's
`NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT`).
Proof for Lemma 1.4
uses 0

From the simple pole of \zeta_K at s = 1 (mathlib's NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT): (s-1)\zeta_K(s) \to r > 0 (the residue, dedekindZeta_residue_pos), so \log\zeta_K(s) - \log(1/(s-1)) = \log\bigl((s-1)\zeta_K(s)\bigr) converges to \log r and is therefore bounded near 1.

Lemma1.5
Statement uses 2
Statement dependency previews
Preview
Lemma 1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

There is a constant C such that, for s > 1 in a right neighbourhood of 1, \sum_{\mathfrak{p}} \Norm\mathfrak{p}^{-s} \;\ge\; \log\frac{1}{s-1} - C.

Lemma 1.3 Lemma 1.4

Lean code for Lemma1.5●1 theorem
  • theoremdefined in CebotarevDensity/Density.lean
    complete
    theorem Chebotarev.log_minus_bounded_le_primeIdealZetaSum.{u_1} (K : Type u_1)
  [Field K] [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1),
      Real.log (1 / (s - 1)) - C ≤
        Chebotarev.primeIdealZetaSum Set.univ s
    theorem Chebotarev.log_minus_bounded_le_primeIdealZetaSum.{u_1}
  (K : Type u_1) [Field K]
  [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in
      nhdsWithin 1 (Set.Ioi 1),
      Real.log (1 / (s - 1)) - C ≤
        Chebotarev.primeIdealZetaSum
          Set.univ s
    Sharifi 7.1.12 proof (p. 140), lower bound: `log(1/(s-1)) - C ≤ Σ_𝔭 N𝔭^{-s}`.
Proof for Lemma 1.5
Proof uses 2
Proof dependency previews
Preview
Lemma 1.3
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

Chain the two identities Lemma 1.3 and Lemma 1.4: \sum_\mathfrak{p} \Norm\mathfrak{p}^{-s} \ge \log\zeta_K(s) - C_1 \ge \log(1/(s-1)) - C_1 - C_2.

Lemma 1.3 Lemma 1.4

Lemma1.6
Statement uses 2
Statement dependency previews
Preview
Lemma 1.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 1✓L∃∀N

There is a constant C' such that, for s > 1 in a right neighbourhood of 1, \sum_{\mathfrak{p}} \Norm\mathfrak{p}^{-s} \;\le\; \log\frac{1}{s-1} + C'.

Lemma 1.3 Lemma 1.4

Lean code for Lemma1.6●1 theorem
  • theoremdefined in CebotarevDensity/Density.lean
    complete
    theorem Chebotarev.primeIdealZetaSum_le_log_plus_bounded.{u_1} (K : Type u_1)
  [Field K] [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1),
      Chebotarev.primeIdealZetaSum Set.univ s ≤
        Real.log (1 / (s - 1)) + C
    theorem Chebotarev.primeIdealZetaSum_le_log_plus_bounded.{u_1}
  (K : Type u_1) [Field K]
  [NumberField K] :
  ∃ C,
    ∀ᶠ (s : ℝ) in
      nhdsWithin 1 (Set.Ioi 1),
      Chebotarev.primeIdealZetaSum
          Set.univ s ≤
        Real.log (1 / (s - 1)) + C
    Sharifi 7.1.12 proof (p. 140), upper bound: `Σ_𝔭 N𝔭^{-s} ≤ log(1/(s-1)) + C'`.
Proof for Lemma 1.6
Proof uses 2
Proof dependency previews
Preview
Lemma 1.3
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

The same two identities Lemma 1.3 and Lemma 1.4, transposed.

Lemma 1.3 Lemma 1.4

Lemma1.7
uses 0used by 1!L∃∀N

Let f : (1, \infty) \to \mathbb{R}. If f is sandwiched as \log\bigl(1/(s-1)\bigr) - C \le f(s) \le \log\bigl(1/(s-1)\bigr) + C' on a right neighbourhood of 1, then f(s)/\log\bigl(1/(s-1)\bigr) \to 1 as s \downarrow 1.

Lean code for Lemma1.7●1 declaration, 1 missing
Proof for Lemma 1.7
uses 0

Since \log\bigl(1/(s-1)\bigr) \to \infty as s \downarrow 1, the additive constants C, C' wash out under division, and the squeeze gives the limit 1.

Lemma1.8
Statement uses 3
Statement dependency previews
Preview
Lemma 1.5
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
Used by 2
Reverse dependency previews
Preview
Lemma 4.7
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

As s \downarrow 1, \sum_{\mathfrak{p}} \Norm\mathfrak{p}^{-s} \sim \log\frac{1}{s-1}.

Lemma 1.5 Lemma 1.6 Lemma 1.7

Lean code for Lemma1.8●1 theorem
  • theoremdefined in CebotarevDensity/Density.lean
    complete
    theorem Chebotarev.primeIdealZetaSum_univ_tendsto_log.{u_1} (K : Type u_1)
  [Field K] [NumberField K] :
  Filter.Tendsto
    (fun s ↦
      Chebotarev.primeIdealZetaSum Set.univ s / Real.log (1 / (s - 1)))
    (nhdsWithin 1 (Set.Ioi 1)) (nhds 1)
    theorem Chebotarev.primeIdealZetaSum_univ_tendsto_log.{u_1}
  (K : Type u_1) [Field K]
  [NumberField K] :
  Filter.Tendsto
    (fun s ↦
      Chebotarev.primeIdealZetaSum
          Set.univ s /
        Real.log (1 / (s - 1)))
    (nhdsWithin 1 (Set.Ioi 1)) (nhds 1)
    **Sharifi 7.1.12**, *Algebraic Number Theory*, p. 140.

The denominator `Σ_𝔭 N𝔭^{-s}` is asymptotic to `log(1/(s-1))` as `s ↓ 1`. This is the analytic
ingredient that makes the Dirichlet-density definition robust under the L-function comparisons in
the Chebotarev proof.
Proof for Lemma 1.8
Proof uses 3
Proof dependency previews
Preview
Lemma 1.5
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

Combine the lower bound Lemma 1.5 and the upper bound Lemma 1.6 into a two-sided \log\bigl(1/(s-1)\bigr) \pm O(1) sandwich, then apply Lemma 1.7 to extract the ratio limit.

Lemma 1.5 Lemma 1.6 Lemma 1.7

  1. 1.1. Density API