Documentation

Mathlib.NumberTheory.VonMangoldt

The von Mangoldt Function #

In this file we define the von Mangoldt function: the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p.

Main Results #

The main definition for this file is

We then prove the classical summation property of the von Mangoldt function in ArithmeticFunction.vonMangoldt_sum, that ∑ i ∈ n.divisors, Λ i = Real.log n, and use this to deduce alternative expressions for the von Mangoldt function via Möbius inversion, see ArithmeticFunction.sum_moebius_mul_log_eq.

Notation #

We use the standard notation Λ to represent the von Mangoldt function. It is accessible in the locales ArithmeticFunction (like the notations for other arithmetic functions) and also in the locale ArithmeticFunction.vonMangoldt.

log as an arithmetic function ℕ → ℝ. Note this is in the ArithmeticFunction namespace to indicate that it is bundled as an ArithmeticFunction rather than being the usual real logarithm.

Equations
Instances For
    @[simp]
    theorem ArithmeticFunction.log_apply {n : } :
    ArithmeticFunction.log n = Real.log n

    The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. In the case when n is a prime power, min_fac will give the appropriate prime, as it is the smallest prime factor.

    In the ArithmeticFunction locale, we have the notation Λ for this function. This is also available in the ArithmeticFunction.vonMangoldt locale, allowing for selective access to the notation.

    Equations
    Instances For

      The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. In the case when n is a prime power, min_fac will give the appropriate prime, as it is the smallest prime factor.

      In the ArithmeticFunction locale, we have the notation Λ for this function. This is also available in the ArithmeticFunction.vonMangoldt locale, allowing for selective access to the notation.

      Equations
      Instances For

        The vonMangoldt function is the function on natural numbers that returns log p if the input can be expressed as p^k for a prime p. In the case when n is a prime power, min_fac will give the appropriate prime, as it is the smallest prime factor.

        In the ArithmeticFunction locale, we have the notation Λ for this function. This is also available in the ArithmeticFunction.vonMangoldt locale, allowing for selective access to the notation.

        Equations
        Instances For
          theorem ArithmeticFunction.vonMangoldt_apply {n : } :
          ArithmeticFunction.vonMangoldt n = if IsPrimePow n then Real.log n.minFac else 0
          @[simp]
          theorem ArithmeticFunction.vonMangoldt_apply_one :
          ArithmeticFunction.vonMangoldt 1 = 0
          @[simp]
          theorem ArithmeticFunction.vonMangoldt_nonneg {n : } :
          0 ArithmeticFunction.vonMangoldt n
          theorem ArithmeticFunction.vonMangoldt_apply_pow {n : } {k : } (hk : k 0) :
          ArithmeticFunction.vonMangoldt (n ^ k) = ArithmeticFunction.vonMangoldt n
          theorem ArithmeticFunction.vonMangoldt_apply_prime {p : } (hp : Nat.Prime p) :
          ArithmeticFunction.vonMangoldt p = Real.log p
          theorem ArithmeticFunction.vonMangoldt_ne_zero_iff {n : } :
          ArithmeticFunction.vonMangoldt n 0 IsPrimePow n
          theorem ArithmeticFunction.vonMangoldt_pos_iff {n : } :
          0 < ArithmeticFunction.vonMangoldt n IsPrimePow n
          theorem ArithmeticFunction.vonMangoldt_eq_zero_iff {n : } :
          ArithmeticFunction.vonMangoldt n = 0 ¬IsPrimePow n
          theorem ArithmeticFunction.vonMangoldt_sum {n : } :
          in.divisors, ArithmeticFunction.vonMangoldt i = Real.log n
          theorem ArithmeticFunction.sum_moebius_mul_log_eq {n : } :
          dn.divisors, (ArithmeticFunction.moebius d) * ArithmeticFunction.log d = -ArithmeticFunction.vonMangoldt n
          theorem ArithmeticFunction.vonMangoldt_le_log {n : } :
          ArithmeticFunction.vonMangoldt n Real.log n