The ideal von Mangoldt function #
The von Mangoldt function of a nonzero ideal A of the ring of integers of a number field is
log N(P) when A is a positive power of a prime ideal P, and zero otherwise. This file
packages that function as an IdealArithmeticFunction and defines its pointwise product with an
ideal arithmetic function.
Main definitions #
TauCeti.IdealArithmeticFunction.vonMangoldtis the complex-valued ideal von Mangoldt function.TauCeti.IdealArithmeticFunction.vonMangoldtTransformsendsfto the weighted functionA ↦ f(A) Λ(A).
Main results #
TauCeti.IdealArithmeticFunction.vonMangoldt_apply_prime_powcomputes the value on a positive power of a prime ideal.TauCeti.IdealArithmeticFunction.vonMangoldt_ne_zero_iffsays that its support is exactly the prime-power ideals.TauCeti.IdealArithmeticFunction.vonMangoldtTransform_ne_zero_iffidentifies the support of the transform, and its specialization inTauCeti.MultiplicativeIdealWeightdescribes this as the good prime powers for a completely multiplicative weight.
The definition chooses a prime base from a proof that A is a prime power. Mathlib's
eq_of_prime_pow_eq, applied to ideals, identifies that choice with any prime base supplied by a
caller. The public evaluation theorem therefore removes the choice from every computation.
Implementation notes #
This is the ideal analogue of Mathlib's ArithmeticFunction.vonMangoldt. Here the prime base is
chosen from IsPrimePow rather than computed by Nat.minFac, its logarithmic weight is
Ideal.absNorm P rather than p, and the function is complex-valued to match
IdealArithmeticFunction.
Roadmap role #
This is the algebraic part of Layer 2.3 of
TauCetiRoadmap/ArithmeticDirichletSeries/README.md. The logarithmic-derivative identity named in
that target additionally requires the Euler-product package of Layer 3; this file supplies its
coefficient and exact prime-power support in advance.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VII.
- G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.
The absolute norm of a prime ideal is greater than one.
The ideal von Mangoldt function. It takes the value log N(P) on every positive power of
a prime ideal P, and vanishes on ideals which are not prime powers.
The codomain is ℂ, matching IdealArithmeticFunction, although every value is real.
Equations
- TauCeti.IdealArithmeticFunction.vonMangoldt A = if h : IsPrimePow ↑A then ↑(Real.log ↑(Ideal.absNorm (Exists.choose h))) else 0
Instances For
The ideal von Mangoldt function vanishes at the unit ideal.
The value of the ideal von Mangoldt function at a positive power of a prime ideal. This is the
choice-free characterization of vonMangoldt on its support.
The ideal von Mangoldt function at a positive power of a prime nonzero ideal.
The ideal von Mangoldt function at a prime ideal.
The ideal von Mangoldt function vanishes away from prime powers.
The support of the ideal von Mangoldt function is exactly the set of prime-power ideals.
The ideal von Mangoldt function vanishes exactly away from prime powers.
Every value of the ideal von Mangoldt function is real.
The (real) values of the ideal von Mangoldt function are nonnegative.
The von Mangoldt function is bounded by the logarithm of the norm. On a power P ^ n its
value is log N(P), and the norm of the ideal is N(P) ^ n with n ≥ 1, so the bound is the
inequality log N(P) ≤ n log N(P); off the prime powers the function vanishes and the logarithm is
still nonnegative.
This is the ideal analogue of ArithmeticFunction.vonMangoldt_le_log, and it is what compares a
von Mangoldt weighted ideal term against the log N(I) weighted terms of
TauCeti.summable_log_absNorm_mul_norm_idealTerm_of_re_lt_re.
The von Mangoldt transform of an ideal arithmetic function f: the pointwise product
A ↦ f(A) Λ(A).
Instances For
Evaluation of the von Mangoldt transform.
The von Mangoldt transform on a positive power of a prime ideal.
The support of a von Mangoldt transform is the intersection of the support of the original function with the prime-power ideals.
The transform of the constant-one ideal arithmetic function is the ideal von Mangoldt function.
The von Mangoldt transform of a completely multiplicative weight on a positive power of a prime ideal.
The support of the von Mangoldt transform of a completely multiplicative weight consists exactly of the prime powers on which the weight is good.