One-sided bounds for Dirichlet density

For a set S of nonzero prime ideals of a number field, Mathlib's NumberField.Set.HasDirichletDensity S δ says that the ratio

S.primeIdealZetaSum s / Set.univ.primeIdealZetaSum s

tends to δ as s approaches 1 from the right. Squeeze arguments often produce the two sides of this limit separately. This file records those one-sided conclusions as NumberField.Set.IsLowerDirichletDensityBound S δ and NumberField.Set.IsUpperDirichletDensityBound S δ.

The predicates use eventual epsilon inequalities, rather than assigning junk-valued lower and upper densities. They are monotone in the proposed bound, and a common lower and upper bound forces a Dirichlet density. A lower bound is always at most an upper bound; this comparison also gives the natural interval restrictions on one-sided bounds.

Main results

• NumberField.Set.hasDirichletDensity_iff: Mathlib's HasDirichletDensity, unfolded to the convergence of the defining ratio.
• NumberField.Set.HasDirichletDensity.isLowerDirichletDensityBound and NumberField.Set.HasDirichletDensity.isUpperDirichletDensityBound: a Dirichlet density is both a lower and an upper bound.
• NumberField.Set.isLowerDirichletDensityBound_of_forall_lt and NumberField.Set.isUpperDirichletDensityBound_of_forall_gt: a value is a lower (upper) bound as soon as every smaller (larger) value is.
• NumberField.Set.IsLowerDirichletDensityBound.le_of_isUpperDirichletDensityBound: every lower bound is at most every upper bound.
• NumberField.Set.hasDirichletDensity_of_upperBound_of_lowerBound: matching one-sided bounds force a Dirichlet density.
• NumberField.Set.hasDirichletDensity_iff_bounds: the resulting characterization of Dirichlet density.

References

• J.-P. Serre, Corps locaux, Chapter VI.
• J. Neukirch, Algebraic Number Theory, Chapter VII.

theorem NumberField.Set.hasDirichletDensity_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} : HasDirichletDensity S δ ↔ Filter.Tendsto (fun (s : ℝ) => primeIdealZetaSum S s / primeIdealZetaSum Set.univ s) (nhdsWithin 1 (Set.Ioi 1)) (nhds δ)

Unfolds HasDirichletDensity S δ to the convergence, as s → 1⁺, of the ratio of the partial prime sum over S to the sum over all primes.

def NumberField.Set.IsLowerDirichletDensityBound {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (δ : ℝ) : Prop

A real number δ is a lower Dirichlet-density bound for S if, for every positive ε, the ratio defining Dirichlet density is eventually strictly above δ - ε as s → 1⁺.

Equations

• One or more equations did not get rendered due to their size.

def NumberField.Set.IsUpperDirichletDensityBound {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (δ : ℝ) : Prop

A real number δ is an upper Dirichlet-density bound for S if, for every positive ε, the ratio defining Dirichlet density is eventually strictly below δ + ε as s → 1⁺.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Set.isLowerDirichletDensityBound_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} : IsLowerDirichletDensityBound S δ ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1), δ - ε < primeIdealZetaSum S s / primeIdealZetaSum Set.univ s

Characteristic restatement of a lower Dirichlet-density bound.

theorem NumberField.Set.isUpperDirichletDensityBound_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} : IsUpperDirichletDensityBound S δ ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (s : ℝ) in nhdsWithin 1 (Set.Ioi 1), primeIdealZetaSum S s / primeIdealZetaSum Set.univ s < δ + ε

Characteristic restatement of an upper Dirichlet-density bound.

theorem NumberField.Set.primeIdealZetaSum_div_univ_nonneg {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (s : ℝ) : 0 ≤ primeIdealZetaSum S s / primeIdealZetaSum Set.univ s

The ratio used to define Dirichlet density is nonnegative at every real parameter.

theorem NumberField.Set.primeIdealZetaSum_div_univ_le_one {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (s : ℝ) : primeIdealZetaSum S s / primeIdealZetaSum Set.univ s ≤ 1

The ratio used to define Dirichlet density is at most one at every real parameter.

@[simp]

theorem NumberField.Set.isLowerDirichletDensityBound_zero {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) : IsLowerDirichletDensityBound S 0

Zero is a lower Dirichlet-density bound for every set of primes.

@[simp]

theorem NumberField.Set.isUpperDirichletDensityBound_one {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) : IsUpperDirichletDensityBound S 1

One is an upper Dirichlet-density bound for every set of primes.

theorem NumberField.Set.IsLowerDirichletDensityBound.mono {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ δ' : ℝ} (h : IsLowerDirichletDensityBound S δ) (hδ : δ' ≤ δ) : IsLowerDirichletDensityBound S δ'

A lower Dirichlet-density bound remains a lower bound when its value is decreased.

theorem NumberField.Set.isLowerDirichletDensityBound_of_forall_lt {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : ∀ δ' < δ, IsLowerDirichletDensityBound S δ') : IsLowerDirichletDensityBound S δ

If every value below δ is a lower Dirichlet-density bound for S, then so is δ.

theorem NumberField.Set.IsUpperDirichletDensityBound.mono {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ δ' : ℝ} (h : IsUpperDirichletDensityBound S δ) (hδ : δ ≤ δ') : IsUpperDirichletDensityBound S δ'

An upper Dirichlet-density bound remains an upper bound when its value is increased.

theorem NumberField.Set.isUpperDirichletDensityBound_of_forall_gt {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : ∀ δ' > δ, IsUpperDirichletDensityBound S δ') : IsUpperDirichletDensityBound S δ

If every value above δ is an upper Dirichlet-density bound for S, then so is δ.

theorem NumberField.Set.HasDirichletDensity.isLowerDirichletDensityBound {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : HasDirichletDensity S δ) : IsLowerDirichletDensityBound S δ

A Dirichlet density is a lower Dirichlet-density bound.

theorem NumberField.Set.HasDirichletDensity.isUpperDirichletDensityBound {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : HasDirichletDensity S δ) : IsUpperDirichletDensityBound S δ

A Dirichlet density is an upper Dirichlet-density bound.

theorem NumberField.Set.IsLowerDirichletDensityBound.le_of_isUpperDirichletDensityBound {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ η : ℝ} (hlower : IsLowerDirichletDensityBound S δ) (hupper : IsUpperDirichletDensityBound S η) : δ ≤ η

Every lower Dirichlet-density bound is at most every upper Dirichlet-density bound for the same set of primes.

theorem NumberField.Set.IsLowerDirichletDensityBound.le_one {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : IsLowerDirichletDensityBound S δ) : δ ≤ 1

A lower Dirichlet-density bound cannot exceed 1.

theorem NumberField.Set.IsUpperDirichletDensityBound.nonneg {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (h : IsUpperDirichletDensityBound S δ) : 0 ≤ δ

An upper Dirichlet-density bound cannot be negative.

theorem NumberField.Set.hasDirichletDensity_of_upperBound_of_lowerBound {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} (hupper : IsUpperDirichletDensityBound S δ) (hlower : IsLowerDirichletDensityBound S δ) : HasDirichletDensity S δ

Matching lower and upper Dirichlet-density bounds force a Dirichlet density equal to their common value.

theorem NumberField.Set.hasDirichletDensity_iff_bounds {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {δ : ℝ} : HasDirichletDensity S δ ↔ IsUpperDirichletDensityBound S δ ∧ IsLowerDirichletDensityBound S δ

A set of primes has Dirichlet density δ exactly when δ is both an upper and a lower Dirichlet-density bound for it.