The Chebotarev Density Theorem in Lean

1.1. Density API🔗

The following routine API lemmas are used by the proofs of the corollaries in the final chapter.

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

A finite set of prime ideals has Dirichlet density 0.

Definition 1.1

Lean code for Lemma1.1.1●1 theorem
  • theoremdefined in CebotarevDensity/Density.lean
    complete
    theorem Chebotarev.hasDirichletDensity_of_finite.{u_1} (K : Type u_1) [Field K]
  [NumberField K] {S : Set (Ideal (NumberField.RingOfIntegers K))}
  (hS : S.Finite) : Chebotarev.HasDirichletDensity S 0
    theorem Chebotarev.hasDirichletDensity_of_finite.{u_1}
  (K : Type u_1) [Field K] [NumberField K]
  {S :
    Set
      (Ideal
        (NumberField.RingOfIntegers K))}
  (hS : S.Finite) :
  Chebotarev.HasDirichletDensity S 0
    **Density of a finite set of primes is `0`** (Sharifi 7.1.13). The numerator `Σ_{𝔭 ∈ S} N𝔭^{-s}`
is bounded (finitely many terms, each `≤ 1`) while the denominator `Σ_𝔭 N𝔭^{-s} → ∞`, so the ratio
`→ 0`.
Proof for Lemma 1.1.1
uses 0

The numerator \sum_{\mathfrak{p} \in S} \Norm\mathfrak{p}^{-s} is bounded as s \to 1^+ (a finite sum of bounded terms), while the denominator \sum_\mathfrak{p} \Norm\mathfrak{p}^{-s} \to \infty by Lemma 1.8; the ratio tends to 0.

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

If S has Dirichlet density \delta, then its lower Dirichlet density is also \delta.

Definition 1.1

Lean code for Lemma1.1.2●1 theorem
  • theoremdefined in CebotarevDensity/Density.lean
    complete
    theorem Chebotarev.HasDirichletDensity.hasLower.{u_1} {K : Type u_1} [Field K]
  [NumberField K] {S : Set (Ideal (NumberField.RingOfIntegers K))}
  {δ : ℝ} (h : Chebotarev.HasDirichletDensity S δ) :
  Chebotarev.HasLowerDirichletDensity S δ
    theorem Chebotarev.HasDirichletDensity.hasLower.{u_1}
  {K : Type u_1} [Field K] [NumberField K]
  {S :
    Set
      (Ideal
        (NumberField.RingOfIntegers K))}
  {δ : ℝ}
  (h :
    Chebotarev.HasDirichletDensity S δ) :
  Chebotarev.HasLowerDirichletDensity S δ
    The lower Dirichlet density extracted from `HasDirichletDensity`.
Proof for Lemma 1.1.2
uses 0

Convergence of the ratio implies the liminf and limsup coincide with the limit; specifically the liminf equals \delta.