Chebyshev's ψ for a set of prime ideals, and the removal of the higher prime powers

For a set S of height-one primes of the ring of integers of a number field K, Chebyshev's ψ weights every prime power 𝔭 ^ k with 𝔭 ∈ S and k ≥ 1 by log N(𝔭), while ϑ weights only the primes themselves. This file defines ψ, proves that the difference ψ - ϑ is exactly the higher-prime-power sum estimated in TauCeti/NumberTheory/ArithmeticDirichletSeries/HigherPrimePowers.lean, and spends that estimate on the transfer of an asymptotic ψ(x) = δ x + o(x) to ϑ(x) = δ x + o(x).

Prime powers with k ≥ 2 are kept visible throughout: ψ is defined with all of them present, and their removal is a named hypothesis, TauCeti.HasNegligibleHigherPrimePowers, discharged for the standard logarithmic weight by TauCeti.standardPrimePowerRemoval. A different coefficient system does not get that hypothesis for free; what it has to supply is the domination bound of TauCeti.primePowerSummatory_isLittleO_of_le_higherPrimePowerWeight.

Main definitions

• TauCeti.primePowerWeight is the standard logarithmic prime-power weight, the value log N(𝔭) at 𝔭 ^ k for every k ≥ 1. It is the real form of the ideal von Mangoldt function of Layer 2 on the prime powers.
• TauCeti.primePsi is its inclusive summatory function over the prime powers whose base lies in S: the number-field analogue of Chebyshev's ψ.
• TauCeti.HasNegligibleHigherPrimePowers K S says that ψ - ϑ is o(x).
• TauCeti.primeVonMangoldtWeight is the same weight spread over all nonzero ideals, zero away from the prime powers with base in S, and TauCeti.primeVonMangoldtCoeff is its regrouping by absolute norm, an ArithmeticFunction ℝ.

Main results

• TauCeti.primePowerSummatory_indicator_sub_primeTheta splits the exponent-one part off the standard weight restricted to any set of prime powers containing exactly the primes of S.
• TauCeti.primePsi_sub_primeTheta identifies ψ - ϑ with the higher-prime-power sum.
• TauCeti.primePsi_le_ncard_mul_log: for x ≥ 1, a finite set of primes contributes at most #S · log x to ψ, with TauCeti.primePsi_isBigO_log_of_finite and TauCeti.primePsi_isLittleO_of_finite its asymptotic forms.
• TauCeti.standardPrimePowerRemoval proves HasNegligibleHigherPrimePowers K S for every S, from the Layer 5 estimate ψ(x) - ϑ(x) = O(√x log² x).
• TauCeti.primeTheta_asymptotic_of_primePsi and TauCeti.primePsi_asymptotic_of_primeTheta transfer a linear asymptotic across that difference, with TauCeti.primeTheta_isEquivalent_of_primePsi the equivalence form for a nonzero density.
• TauCeti.primePsi_eq_sum_range presents ψ(x) as the inclusive partial sum ∑_{n ≤ ⌊x⌋₊} a n of the coefficient system, whose coefficients are nonnegative (TauCeti.primeVonMangoldtCoeff_nonneg) and supported on the prime powers (TauCeti.primeVonMangoldtCoeff_eq_zero_of_not_isPrimePow).
• TauCeti.normCoeff_vonMangoldt identifies the coefficient system of the full prime carrier with the Layer 1 regrouping of the Layer 2 ideal von Mangoldt function.
• TauCeti.primeVonMangoldtCoeff_rat_natGenerator_pow evaluates the coefficient system of any set of primes of 𝓞 ℚ at a prime power, and TauCeti.primeVonMangoldtCoeff_rat_le bounds it by Mathlib's von Mangoldt function Λ.

Roadmap role

This is Layer 10.2 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md: "For the fixed standard nonnegative logarithmic prime-power weight, use Layer 5 to prove standardPrimePowerRemoval : HasNegligibleHigherPrimePowers K S and make primeTheta_asymptotic_of_primePsi consume that named estimate." It also supplies the arithmetic half of Layer 10.1, "Define primePsi with all prime powers present": the exact nonnegative von Mangoldt coefficient system and the identity presenting ψ as its partial sum, which is the shape in which a Tauberian theorem delivers its conclusion. The analytic boundary package and the resulting prime-number-theorem transfer are in TauCeti/NumberTheory/ArithmeticDirichletSeries/Prime/Boundary.lean.

References

• H. Davenport, Multiplicative Number Theory, Chapter 7.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.
• J. Neukirch, Algebraic Number Theory, Chapter VII.

The rational-prime case of ψ, ϑ and their difference is Mathlib's Mathlib/NumberTheory/Chebyshev.lean, whose Chebyshev.theta_le_psi and Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log are the analogues of TauCeti.primeTheta_le_primePsi and TauCeti.standardPrimePowerRemoval; nothing is transported from there, since the estimate consumed here is proved over prime ideals in Layer 5.

The standard logarithmic prime-power weight

noncomputable def TauCeti.primePowerWeight {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : ℝ

The standard logarithmic prime-power weight: the value log N(𝔭) at the prime power 𝔭 ^ k, for every k ≥ 1. Unlike TauCeti.higherPrimePowerWeight it does not vanish on the primes themselves, so its summatory function is Chebyshev's ψ rather than ψ - ϑ.

Equations

• TauCeti.primePowerWeight A = Real.log ↑(Ideal.absNorm (TauCeti.primePowerBase A).asIdeal)

theorem TauCeti.primePowerWeight_eq_vonMangoldt_re {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : primePowerWeight A = (IdealArithmeticFunction.vonMangoldt ↑A).re

The standard logarithmic prime-power weight is the real part of the ideal von Mangoldt function of Layer 2, restricted to the prime powers.

@[simp]

theorem TauCeti.vonMangoldt_eq_primePowerWeight {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : IdealArithmeticFunction.vonMangoldt ↑A = ↑(primePowerWeight A)

On a prime-power ideal the ideal von Mangoldt function is the standard logarithmic weight, as a complex number.

theorem TauCeti.primePowerWeight_pos {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : 0 < primePowerWeight A

The standard logarithmic prime-power weight is positive.

theorem TauCeti.primePowerWeight_nonneg {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : 0 ≤ primePowerWeight A

The standard logarithmic prime-power weight is nonnegative.

@[simp]

theorem TauCeti.primePowerWeight_ofPrime {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : primePowerWeight (IdealPrimePower.ofPrime v) = Real.log ↑(Ideal.absNorm v.asIdeal)

On a prime the standard weight is the logarithm of its own absolute norm.

theorem TauCeti.higherPrimePowerWeight_of_not_prime {K : Type u_1} [Field K] [NumberField K] {A : IdealPrimePower K} (hA : ¬Prime ↑↑A) : higherPrimePowerWeight A = primePowerWeight A

Away from the primes the two prime-power weights agree: TauCeti.higherPrimePowerWeight is the standard weight with its exponent-one part deleted.

Chebyshev's ψ

noncomputable def TauCeti.primePsi (K : Type u_1) [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : ℝ

Chebyshev's ψ for a set of prime ideals: the inclusive sum of log N(𝔭) over the prime powers 𝔭 ^ k of absolute norm at most x whose base 𝔭 lies in S, with every exponent k ≥ 1 present.

Equations

• TauCeti.primePsi K S x = TauCeti.primePowerSummatory K ({A : TauCeti.IdealPrimePower K | TauCeti.primePowerBase A ∈ S}.indicator TauCeti.primePowerWeight) x

theorem TauCeti.primePsi_apply {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : primePsi K S x = ∑ A ∈ primePowersLE K x, {A : IdealPrimePower K | primePowerBase A ∈ S}.indicator primePowerWeight A

Chebyshev's ψ as an explicit sum over the inclusive prime-power carrier.

@[simp]

theorem TauCeti.primePsi_empty {K : Type u_1} [Field K] [NumberField K] (x : ℝ) : primePsi K ∅ x = 0

The empty set of primes contributes nothing to ψ.

theorem TauCeti.primePsi_nonneg {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : 0 ≤ primePsi K S x

Chebyshev's ψ is nonnegative.

theorem TauCeti.primePsi_mono {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : Monotone (primePsi K S)

Chebyshev's ψ is monotone in the inclusive cutoff.

theorem TauCeti.primePsi_eq_zero_of_lt_two {K : Type u_1} [Field K] [NumberField K] {x : ℝ} (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hx : x < 2) : primePsi K S x = 0

Below the cutoff 2 there is no prime power to weight.

The higher prime powers as the gap between ψ and ϑ

theorem TauCeti.primePowerSummatory_indicator_sub_primeTheta {K : Type u_1} [Field K] [NumberField K] (T : Set (IdealPrimePower K)) (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hTS : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), IdealPrimePower.ofPrime v ∈ T ↔ v ∈ S) (x : ℝ) : primePowerSummatory K (T.indicator primePowerWeight) x - primeTheta K S x = primePowerSummatory K (T.indicator higherPrimePowerWeight) x

Splitting the exponent-one part off a restricted prime-power sum. For a set T of prime powers containing exactly the primes of S, the summatory function of the standard logarithmic weight restricted to T exceeds ϑ by the higher-prime-power sum over T.

theorem TauCeti.primePsi_sub_primeTheta {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : primePsi K S x - primeTheta K S x = primePowerSummatory K ({A : IdealPrimePower K | primePowerBase A ∈ S}.indicator higherPrimePowerWeight) x

The difference between ψ and ϑ is the higher-prime-power sum. Both sides run over the prime powers whose base lies in S; the exponent-one part of ψ is exactly ϑ.

theorem TauCeti.primeTheta_le_primePsi {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : primeTheta K S x ≤ primePsi K S x

Chebyshev's ϑ never exceeds ψ.

Removing the higher prime powers

def TauCeti.HasNegligibleHigherPrimePowers (K : Type u_1) [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : Prop

The higher prime powers of S are negligible: ψ - ϑ is o(x). Naming the hypothesis keeps the estimate an input to the prime-number-theorem transfer instead of a definitional simplification of ψ.

Equations

• TauCeti.HasNegligibleHigherPrimePowers K S = (fun (x : ℝ) => TauCeti.primePsi K S x - TauCeti.primeTheta K S x) =o[Filter.atTop] fun (x : ℝ) => x

theorem TauCeti.hasNegligibleHigherPrimePowers_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} : HasNegligibleHigherPrimePowers K S ↔ (fun (x : ℝ) => primePsi K S x - primeTheta K S x) =o[Filter.atTop] fun (x : ℝ) => x

The defining little-o estimate behind TauCeti.HasNegligibleHigherPrimePowers.

theorem TauCeti.standardPrimePowerRemoval (K : Type u_2) [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : HasNegligibleHigherPrimePowers K S

Removal of the higher prime powers for the standard logarithmic weight. This is the o(x) corollary of the Layer 5 bound ψ(x) - ϑ(x) ≤ [K:ℚ] / (2 log 2) · √x log² x.

theorem TauCeti.primePsi_le_ncard_mul_log {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {x : ℝ} (hS : S.Finite) (hx : 1 ≤ x) : primePsi K S x ≤ ↑S.ncard * Real.log x

For x ≥ 1, a finite set of primes contributes at most #S · log x to ψ. Fibring over the prime base, the exponents k ≥ 1 with N(𝔭) ^ k ≤ x contribute at most log x in total for each of the finitely many 𝔭.

A counting argument can therefore discard a finite exceptional set of primes — those ramifying in an extension, say, or lying above such — at a cost of O(log x).

The fibre step is TauCeti.card_mul_log_absNorm_le_of_pow_le_of_base_eq, which bounds the total weight of the prime powers over a single base by log x.

theorem TauCeti.primePsi_isBigO_log_of_finite {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : S.Finite) : primePsi K S =O[Filter.atTop] Real.log

A finite set of primes is O(log x) for ψ, the asymptotic form of the bound above.

theorem TauCeti.primePsi_isLittleO_of_finite {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : S.Finite) : primePsi K S =o[Filter.atTop] fun (x : ℝ) => x

A finite set of primes is negligible for ψ, the form the total discard estimate sums.

theorem TauCeti.primeTheta_asymptotic_of_primePsi {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (h : HasNegligibleHigherPrimePowers K S) (hψ : (fun (x : ℝ) => primePsi K S x - δ * x) =o[Filter.atTop] fun (x : ℝ) => x) : (fun (x : ℝ) => primeTheta K S x - δ * x) =o[Filter.atTop] fun (x : ℝ) => x

Transfer of a linear asymptotic from ψ to ϑ. If the higher prime powers of S are negligible and ψ(x) = δ x + o(x), then ϑ(x) = δ x + o(x).

theorem TauCeti.primePsi_asymptotic_of_primeTheta {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (h : HasNegligibleHigherPrimePowers K S) (hϑ : (fun (x : ℝ) => primeTheta K S x - δ * x) =o[Filter.atTop] fun (x : ℝ) => x) : (fun (x : ℝ) => primePsi K S x - δ * x) =o[Filter.atTop] fun (x : ℝ) => x

Transfer of a linear asymptotic from ϑ to ψ, the converse direction.

theorem TauCeti.primeTheta_isEquivalent_of_primePsi {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ} (hδ : δ ≠ 0) (h : HasNegligibleHigherPrimePowers K S) (hψ : Asymptotics.IsEquivalent Filter.atTop (primePsi K S) fun (x : ℝ) => δ * x) : Asymptotics.IsEquivalent Filter.atTop (primeTheta K S) fun (x : ℝ) => δ * x

The asymptotic-equivalence form of TauCeti.primeTheta_asymptotic_of_primePsi, for a nonzero density δ. At δ = 0 an equivalence would force ϑ to vanish eventually, so the o(x) form above is the one that covers that case.

The von Mangoldt coefficient system of a set of primes

noncomputable def TauCeti.primeVonMangoldtWeight (K : Type u_1) [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : ℝ

The von Mangoldt weight of a set S of height-one primes, as a real weight on the nonzero integral ideals of 𝓞 K: the value log N(𝔭) at 𝔭 ^ k for 𝔭 ∈ S and k ≥ 1, and 0 at every other nonzero ideal.

It is the ideal von Mangoldt function of Layer 2 cut down to the prime powers whose base lies in S, taken in its real form, because the Tauberian input of Layer 9 is a nonnegative real coefficient system. Cutting down by "some prime of S divides A" rather than by the prime base of A avoids naming that base at ideals which are not prime powers, where the ideal von Mangoldt function vanishes anyway.

Equations

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

theorem TauCeti.primeVonMangoldtWeight_of_exists_dvd {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (h : ∃ 𝔭 ∈ S, 𝔭.asIdeal ∣ ↑A) : primeVonMangoldtWeight K S A = (IdealArithmeticFunction.vonMangoldt A).re

At an ideal divisible by a prime of S, the von Mangoldt weight of S is the ideal von Mangoldt value.

theorem TauCeti.primeVonMangoldtWeight_of_not_exists_dvd {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (h : ¬∃ 𝔭 ∈ S, 𝔭.asIdeal ∣ ↑A) : primeVonMangoldtWeight K S A = 0

The von Mangoldt weight of S vanishes at an ideal with no prime factor in S.

@[simp]

theorem TauCeti.primeVonMangoldtWeight_empty {K : Type u_1} [Field K] [NumberField K] (A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : primeVonMangoldtWeight K ∅ A = 0

The empty set of primes carries no von Mangoldt weight.

@[simp]

theorem TauCeti.primeVonMangoldtWeight_eq_zero_of_not_isPrimePow {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : ¬IsPrimePow ↑A) : primeVonMangoldtWeight K S A = 0

The von Mangoldt weight of S vanishes away from the prime-power ideals.

theorem TauCeti.primeVonMangoldtWeight_nonneg {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : 0 ≤ primeVonMangoldtWeight K S A

The von Mangoldt weight of S is nonnegative.

theorem TauCeti.primeVonMangoldtWeight_of_pow_of_mem {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (h𝔭 : 𝔭 ∈ S) {k : ℕ} (hk : 0 < k) {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : 𝔭.asIdeal ^ k = ↑A) : primeVonMangoldtWeight K S A = Real.log ↑(Ideal.absNorm 𝔭.asIdeal)

The von Mangoldt weight of S at a positive power of a prime of S.

theorem TauCeti.primeVonMangoldtWeight_of_pow_of_notMem {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (h𝔭 : 𝔭 ∉ S) {k : ℕ} (hk : 0 < k) {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hA : 𝔭.asIdeal ^ k = ↑A) : primeVonMangoldtWeight K S A = 0

The von Mangoldt weight of S vanishes at a positive power of a prime outside S.

theorem TauCeti.primeVonMangoldtWeight_mono_set {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hST : S ⊆ T) (A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : primeVonMangoldtWeight K S A ≤ primeVonMangoldtWeight K T A

The von Mangoldt weight is monotone in the set of primes.

theorem TauCeti.primeVonMangoldtWeight_idealPrimePower {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (A : IdealPrimePower K) : primeVonMangoldtWeight K S ↑A = {B : IdealPrimePower K | primePowerBase B ∈ S}.indicator primePowerWeight A

The von Mangoldt weight of S on the prime-power carrier is exactly the summand of Chebyshev's ψ: the standard logarithmic weight at the prime powers with base in S, and 0 elsewhere.

@[simp]

theorem TauCeti.primeVonMangoldtWeight_univ {K : Type u_1} [Field K] [NumberField K] (A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : primeVonMangoldtWeight K Set.univ A = (IdealArithmeticFunction.vonMangoldt A).re

Over all height-one primes the weight is the real form of the ideal von Mangoldt function of Layer 2.

noncomputable def TauCeti.primeVonMangoldtCoeff (K : Type u_1) [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : ArithmeticFunction ℝ

The von Mangoldt coefficient system of a set S of height-one primes: its value at n is the sum of log N(𝔭) over the prime powers 𝔭 ^ k of absolute norm exactly n whose base 𝔭 lies in S.

This is the nonnegative arithmetic function whose inclusive partial sums are Chebyshev's ψ, by TauCeti.primePsi_eq_sum_range, and whose Dirichlet series is the one a Tauberian theorem sees.

Equations

• TauCeti.primeVonMangoldtCoeff K S = { toFun := fun (n : ℕ) => ∑ I ∈ TauCeti.normFiber K n, TauCeti.primeVonMangoldtWeight K S I, map_zero' := ⋯ }

theorem TauCeti.primeVonMangoldtCoeff_apply {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (n : ℕ) : (primeVonMangoldtCoeff K S) n = ∑ I ∈ normFiber K n, primeVonMangoldtWeight K S I

The von Mangoldt coefficient at n is the total weight of the absolute-norm fibre at n.

theorem TauCeti.primeVonMangoldtCoeff_nonneg {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (n : ℕ) : 0 ≤ (primeVonMangoldtCoeff K S) n

The von Mangoldt coefficients are nonnegative, as the Tauberian input requires.

@[simp]

theorem TauCeti.primeVonMangoldtCoeff_empty {K : Type u_1} [Field K] [NumberField K] (n : ℕ) : (primeVonMangoldtCoeff K ∅) n = 0

The empty set of primes has vanishing von Mangoldt coefficients.

@[simp]

theorem TauCeti.primeVonMangoldtCoeff_apply_one {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) : (primeVonMangoldtCoeff K S) 1 = 0

The von Mangoldt coefficient at 1 vanishes: the unit ideal is the only ideal of absolute norm one, and it is not a prime power.

theorem TauCeti.primeVonMangoldtCoeff_mono_set {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hST : S ⊆ T) (n : ℕ) : (primeVonMangoldtCoeff K S) n ≤ (primeVonMangoldtCoeff K T) n

The von Mangoldt coefficients are monotone in the set of primes.

theorem TauCeti.primeVonMangoldtCoeff_eq_zero_of_not_isPrimePow {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) {n : ℕ} (hn : ¬IsPrimePow n) : (primeVonMangoldtCoeff K S) n = 0

The support of the coefficient system: a von Mangoldt coefficient vanishes unless its index is a prime power, since the absolute norm of a prime-power ideal is again a prime power.

theorem TauCeti.normCoeff_ofReal_primeVonMangoldtWeight {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (n : ℕ) : ((normCoeff K) fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => ↑(primeVonMangoldtWeight K S I)) n = ↑((primeVonMangoldtCoeff K S) n)

The coefficient system is the Layer 1 norm regrouping of the von Mangoldt weight of S, read in ℂ.

theorem TauCeti.normCoeff_vonMangoldt {K : Type u_1} [Field K] [NumberField K] (n : ℕ) : ((normCoeff K) IdealArithmeticFunction.vonMangoldt) n = ↑((primeVonMangoldtCoeff K Set.univ) n)

Over all height-one primes the coefficient system regroups the ideal von Mangoldt function of Layer 2 by absolute norm.

theorem TauCeti.primePsi_eq_sum_range {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : primePsi K S x = ∑ n ∈ Finset.range (⌊x⌋₊ + 1), (primeVonMangoldtCoeff K S) n

Chebyshev's ψ is the inclusive partial sum of the von Mangoldt coefficient system.

This is what lets a Tauberian theorem stated for x⁻¹ ∑_{n ≤ x} a n speak about ψ(x) / x: Layer 9's conclusion is about the left-hand side, and Layer 10 needs it about the right.

theorem TauCeti.primePsi_natCast_eq_sum_range {K : Type u_1} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (n : ℕ) : primePsi K S ↑n = ∑ m ∈ Finset.range (n + 1), (primeVonMangoldtCoeff K S) m

Chebyshev's ψ at a natural cutoff, the form in which the coefficient system is summed.

@[simp]

theorem TauCeti.primeVonMangoldtCoeff_rat_natGenerator_pow (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) {k : ℕ} (hk : 0 < k) : (primeVonMangoldtCoeff ℚ S) (Rat.HeightOneSpectrum.natGenerator v ^ k) = if v ∈ S then Real.log ↑(Rat.HeightOneSpectrum.natGenerator v) else 0

Over ℚ, the coefficient at p ^ k, for p the rational prime under v, is log p if v ∈ S and 0 otherwise.

theorem TauCeti.primeVonMangoldtCoeff_rat_le (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ))) (n : ℕ) : (primeVonMangoldtCoeff ℚ S) n ≤ ArithmeticFunction.vonMangoldt n

Over ℚ, the von Mangoldt coefficients of any set of primes are bounded by Λ.