moebius-sq-LSeries-eulerProduct-… to LSeries totient eq

Theoremmoebius-sq-LSeries-eulerProduct-tprod#

For \(1\lt \Re(s)\) we have that

\[ \sum_{1\leq n}\mu^2(n)n^{-s}=\prod_p(1+p^{-s}). \]

The naming convention here is designed to match

riemannZeta_eulerProduct_tprod
Proof

Immediately follows from Lemmas moebius-sq-LSeries.term-IsMultiplicative and moebius-sq-tsum-prime-pow.

Lean

Formalized as ArithmeticFunction.moebius_sq_LSeries_eulerProduct_tprod.

Sources
LeanArithmeticFunction.moebius_sq_LSeries_eulerProduct_tprod
Uses 5 · Used by 1
Proof usesLSeriesSummable-moebius-sq · moebius-sq-tsum-prime-pow · moebius-sq-LSeries.term-isMultiplicative · sumOnPrimePows-apply · sumOnPrimePows
Used byzeta alt

Theoremmoebius-sq-LSeries-eulerProduct-hasProd#

For \(1\lt \Re(s)\) we have that

\[ \sum_{1\leq n}\mu^2(n)n^{-s}=\prod_p(1+p^{-s}). \]

The naming convention here is designed to match

riemannZeta_eulerProduct_hasProd
Proof

Immediately follows from Lemmas moebius-sq-LSeries.term-IsMultiplicative and moebius-sq-tsum-prime-pow.

Lean

Formalized as ArithmeticFunction.moebius_sq_LSeries_eulerProduct_hasProd.

Sources
LeanArithmeticFunction.moebius_sq_LSeries_eulerProduct_hasProd
Uses 3 · Used by 1
Proof usesLSeriesSummable-moebius-sq · moebius-sq-tsum-prime-pow · moebius-sq-LSeries.term-isMultiplicative
Used byzeta alt

Theoremzeta alt#

\[ \zeta(s) =\zeta(2s) \sum_{n=1}^{\infty}\mu^2(n)n^{-s}. \]
An expression for `ζ`, in IK (1.32).
Proof

The series \(\sum_{n=1}^{\infty}\mu^2(n)n^{-s}\) has Euler product \(\prod_{p} (1 + p^{-s})\). On the other hand, \(\zeta(2s)=\prod_p (1 - p^{-2s})^{-1}\). The product of these two Euler products is \(\prod_p (1 - p^{-s})^{-1} = \zeta(s)\), which gives the desired formula.

Lean

Formalized as ArithmeticFunction.zeta_alt.

Sources
LeanArithmeticFunction.zeta_alt
Uses 3
Proof usesmoebius-sq-LSeries-eulerProduct-tprod · moebius-sq-LSeries-eulerProduct-hasProd · Complex.one-add-prime-cpow-ne-zero

Theorempow-divisors-mul#

Let \(m\) and \(n\) be coprime natural numbers and let \(k\) be fixed. The divisors \(x\) of \(mn\) with \(x^k \mid mn\) are exactly the products \(ab\) where \(a \mid m\), \(a^k \mid m\), \(b \mid n\), and \(b^k \mid n\).

Proof

Since \(m\) and \(n\) are coprime, every divisor of \(mn\) factors uniquely as \(ab\) with \(a \mid m\) and \(b \mid n\). For such a factorization, \(x^k \mid mn\) is equivalent to \(a^k \mid m\) and \(b^k \mid n\), again by coprimality.

Lean

Formalized as ArithmeticFunction.pow_divisors_mul.

Sources
LeanArithmeticFunction.pow_divisors_mul
Used by 1
Used bysum-moebius-sq-divisors-is-multiplicative

Theoremdivisors-mul-injective#

Let \(m\) and \(n\) be coprime natural numbers. The function \((a,b) \mapsto ab\) is injective on the product of the divisors of \(m\) and \(n\).

Upstreamed to mathlib via PR #36495.
Proof

Since \(m\) and \(n\) are coprime, any element in the product of their divisors can be uniquely expressed as a product of an element from each set. The injectivity follows from the uniqueness of this decomposition.

Lean

Stated as ArithmeticFunction.divisors_mul_injective; the blueprint marks no proof of it as formalized.

Sources
LeanArithmeticFunction.divisors_mul_injective
Used by 1
Used bypow-divisors-mul-injective

Theorempow-divisors-mul-injective#

Let \(m\) and \(n\) be coprime natural numbers and let \(k\) be fixed. The map \((a,b) \mapsto ab\) is injective on the product of \(\{a \mid m : a^k \mid m\}\) and \(\{b \mid n : b^k \mid n\}\).

Proof

This is the restriction of Lemma divisors-mul-injective to a subset of the divisor product, so injectivity is preserved.

Lean

Formalized as ArithmeticFunction.pow_divisors_mul_injective.

Sources
LeanArithmeticFunction.pow_divisors_mul_injective
Uses 1 · Used by 1
Proof usesdivisors-mul-injective
Used bysum-moebius-sq-divisors-is-multiplicative

Definitionsum-moebius-sq-divisors#

The function \(n \mapsto \sum_{d^2|n} \mu(d)\).

Lean

Formalized as ArithmeticFunction.sum_moebius_sq_divisors.

Sources
LeanArithmeticFunction.sum_moebius_sq_divisors
Used by 4
Used bymoebius-sq-eq · sum-moebius-sq-divisors-apply · sum-moebius-sq-divisors-apply-prime-pow · sum-moebius-sq-divisors-is-multiplicative

Theoremsum-moebius-sq-divisors-apply#

A simple helper lemma for the above definition.

Lean

Formalized as ArithmeticFunction.sum_moebius_sq_divisors_apply.

Sources
LeanArithmeticFunction.sum_moebius_sq_divisors_apply
Uses 1 · Used by 2
Statement usessum-moebius-sq-divisors
Used bymoebius-sq-eq · sum-moebius-sq-divisors-apply-prime-pow

Theoremsum-moebius-sq-divisors-is-multiplicative#

The function \(n \mapsto \sum_{d^2|n} \mu(d)\) is multiplicative.

Proof

We will show that for coprime \(m\) and \(n\), we have \(\sum_{d^2|mn} \mu(d) = \sum_{d^2|m} \mu(d) \cdot \sum_{d^2|n} \mu(d)\). This follows from Lemma pow-divisors-mul: the divisors \(d\) of \(mn\) with \(d^2 \mid mn\) factor uniquely as \(d=ab\) with \(a^2 \mid m\) and \(b^2 \mid n\). Multiplicativity of \(\mu\) then factors the sum.

Lean

Formalized as ArithmeticFunction.sum_moebius_sq_divisors_IsMultiplicative.

Sources
LeanArithmeticFunction.sum_moebius_sq_divisors_IsMultiplicative
Uses 3 · Used by 1
Statement usessum-moebius-sq-divisors
Proof usespow-divisors-mul · pow-divisors-mul-injective
Used bymoebius-sq-eq

Theoremsum-moebius-sq-divisors-apply-prime-pow#

Applied at prime powers, sum-moebius-sq-divisors coincides with \(\mu^2\).

Proof

For a prime power \(p^k\), note that if \(k\leq 1\) then the only square divisor is \(1\), so the sum evaluates as \(\mu(1)=1\). If \(k\geq 2\), then \(1\) and \(p^2\) are square divisors of \(p^k\). Thus, the sum evaluates as \(\mu(1)+\mu(p)+\ldots\) where the remaining terms are moebius of higher powers (if necessary). Since \(\mu(p)=-1\) and \(\mu\) of higher powers of \(p\) is zero, this is \(0\). This agrees with \(\mu(p^k)^2\), which is simply an indicator function for \(k\leq 1\) (i.e. \(p^k\) is squarefree).

Lean

Formalized as ArithmeticFunction.sum_moebius_sq_divisors_apply_prime_pow.

Sources
LeanArithmeticFunction.sum_moebius_sq_divisors_apply_prime_pow
Uses 2 · Used by 1
Statement usessum-moebius-sq-divisors
Proof usessum-moebius-sq-divisors-apply
Used bymoebius-sq-eq

Theoremmoebius-sq-eq#

I-K (1.33): \(\mu^2(n) = \sum_{d^2|n} \mu(d)\).

Proof

Apply the previous two lemmas.

Lean

Formalized as ArithmeticFunction.moebius_sq_eq.

Sources
LeanArithmeticFunction.moebius_sq_eq
Uses 4
Proof usessum-moebius-sq-divisors · sum-moebius-sq-divisors-is-multiplicative · sum-moebius-sq-divisors-apply · sum-moebius-sq-divisors-apply-prime-pow

Theoremliouville#

Liouville function: \(\lambda(n) = (-1)^{\Omega(n)}\).

Proof

The Liouville function \(\lambda(n)\) is defined as \((-1)^{\Omega(n)}\), where \(\Omega(n)\) is the total number of prime factors of \(n\) counted with multiplicity. This means that for each prime factor of \(n\), we contribute a factor of \(-1\) to the product, and the overall sign of \(\lambda(n)\) depends on whether the total number of prime factors is even or odd. Thus, we have \(\lambda(n) = (-1)^{\Omega(n)}\) by definition.

Lean

Formalized as ArithmeticFunction.liouville.

Sources
LeanArithmeticFunction.liouville
Used by 3
Used byisCompletelyMultiplicative liouville · liouville eq moebius on squarefree · LSeries liouville eq

DefinitionIsCompletelyMultiplicative#

Define Complete Multiplicativity for an arithmetic function.

Lean

Formalized as ArithmeticFunction.IsCompletelyMultiplicative.

Sources
LeanArithmeticFunction.IsCompletelyMultiplicative
Used by 2
Used byIsCompletelyMultiplicative.isMultiplicative · isCompletelyMultiplicative liouville

TheoremIsCompletelyMultiplicative.isMultiplicative#

A function that is completely multiplicative is also multiplicative.

Proof

Let \(f\) be a completely multiplicative function. To show that \(f\) is multiplicative, we need to verify that \(f(1) = 1\) and that \(f(ab) = f(a)f(b)\) for all coprime natural numbers \(a\) and \(b\). Since \(f\) is completely multiplicative, we have \(f(1) = 1\) by definition. For coprime \(a\) and \(b\), we can write \(ab\) as a product of prime factors, and since \(f\) is completely multiplicative, it will factor as the product of the values of \(f\) at those prime factors. This means that \(f(ab) = f(a)f(b)\) for coprime \(a\) and \(b\), which shows that \(f\) is multiplicative.

Lean

Formalized as ArithmeticFunction.IsCompletelyMultiplicative.isMultiplicative.

Sources
LeanArithmeticFunction.IsCompletelyMultiplicative.isMultiplicative
Uses 1
Statement usesIsCompletelyMultiplicative

TheoremisCompletelyMultiplicative liouville#

The Liouville function is completely multiplicative.

Proof

The Liouville function \(\lambda(n)\) is defined as \((-1)^{\Omega(n)}\), where \(\Omega(n)\) counts the total number of prime factors of \(n\) with multiplicity. To show that \(\lambda\) is completely multiplicative, we need to verify that \(\lambda(1) = 1\) and that \(\lambda(ab) = \lambda(a)\lambda(b)\) for all natural numbers \(a\) and \(b\).

Lean

Stated as ArithmeticFunction.isCompletelyMultiplicative_liouville; the blueprint marks no proof of it as formalized.

Sources
LeanArithmeticFunction.isCompletelyMultiplicative_liouville
Uses 2
Statement usesliouville · IsCompletelyMultiplicative

TheoremLSeries liouville eq#

The Dirichlet series of the Liouville function is \(\zeta(2s)/\zeta(s)\).

Proof

The Liouville function \(\lambda(n)\) is multiplicative, and its value at prime powers is given by \(\lambda(p^k) = (-1)^k\). The Dirichlet series of \(\lambda\) can be expressed as an Euler product over primes:

\[ L(\lambda, s) = \prod_{p} \left(1 + \lambda(p)p^{-s} + \lambda(p^2)p^{-2s} + \ldots\right) = \prod_{p} \left(1 - p^{-s}\right) \left(1 - p^{-2s}\right)^{-1} = \frac{\zeta(2s)}{\zeta(s)}. \]
Lean

Stated as ArithmeticFunction.LSeries_liouville_eq; the blueprint marks no proof of it as formalized.

Sources
LeanArithmeticFunction.LSeries_liouville_eq
Uses 1
Statement usesliouville

Theoremliouville eq moebius on squarefree#

The Liouville function agrees with the Möbius function on square-free numbers.

Proof

The Liouville function \(\lambda(n)\) is defined as \((-1)^{\Omega(n)}\), where \(\Omega(n)\) counts the total number of prime factors of \(n\) with multiplicity. The Möbius function \(\mu(n)\) is defined as \(0\) if \(n\) has a squared prime factor, and otherwise it is \((-1)^{\omega(n)}\), where \(\omega(n)\) counts the number of distinct prime factors of \(n\). For square-free numbers, we have \(\Omega(n) = \omega(n)\), since there are no repeated prime factors. Therefore, for square-free numbers, we have \(\lambda(n) = (-1)^{\omega(n)} = \mu(n)\), which shows that the Liouville function agrees with the Möbius function on square-free numbers.

Lean

Formalized as ArithmeticFunction.liouville_eq_moebius_on_squarefree.

Sources
LeanArithmeticFunction.liouville_eq_moebius_on_squarefree
Uses 1
Statement usesliouville

TheoremLSeries totient eq#

Euler totient series: \(\sum_{n=1}^{\infty} \varphi(n) n^{-s} = \zeta(s-1)/\zeta(s)\) for \(\Re(s) > 2\).

This is IK (1.35). The L-series converges absolutely for Re(s) > 2
(using φ(n) ≤ n to bound terms; the original hypothesis 1 < Re(s) is incorrect).
Proof

The Euler totient function \(\varphi(n)\) counts the positive integers up to \(n\) that are relatively prime to \(n\). It is a multiplicative function, and its value at prime powers is given by \(\varphi(p^k) = p^k - p^{k-1}\). The Dirichlet series of \(\varphi\) can be expressed as an Euler product over primes:

\[ L(\varphi, s) = \prod_{p} \left(1 + \varphi(p)p^{-s} + \varphi(p^2)p^{-2s} + \ldots\right) = \prod_{p} \left(1 - p^{-s +1}\right)^{-1} \left(1 - p^{-s}\right) = \frac{\zeta(s-1)}{\zeta(s)}. \]

The L-series converges absolutely for Re(s) \(>\) 2, using φ(n) ≤ n to bound the terms.

Lean

Formalized as ArithmeticFunction.LSeries_totient_eq.

Sources
LeanArithmeticFunction.LSeries_totient_eq
Uses 2
Proof usesLSeries powR eq · powR

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.