zeta pow three eq to moebius-sq-tsum-prime-pow
Theoremzeta pow three eq#
Zeta cubed: \(\zeta(s)^3 = \zeta(2s) \sum_{n=1}^{\infty}\tau(n^2) n^{-s}\).
This is IK (1.30).
Proof
This follows from the previous two theorems. From the corollary of Ramanujan's formula, we have \(\zeta(s)^4 = \zeta(2s) \sum_{n=1}^{\infty} \tau(n)^2 n^{-s}\). From the Baby Rankin-Selberg result, we have \(\zeta(s) \sum_{n=1}^{\infty} \tau(n^2) n^{-s} = \sum_{n=1}^{\infty} \tau(n)^2 n^{-s}\). Combining these two results, we can express \(\zeta(s)^4\) in terms of \(\zeta(s)\) and \(\sum_{n=1}^{\infty} \tau(n^ 2) n^{-s}\), which leads to the conclusion that \(\zeta(s)^3 = \zeta(2s) \sum_{n=1}^{\infty} \tau(n^2) n^{-s}\).
Lean
Formalized as ArithmeticFunction.zeta_pow_three_eq'.
Sources
Uses 2
Theoremzeta pow three eq alt#
symmetric square \(L\)-function for \(\zeta^2\):
for \(\Re(s) > 1\).
Alternative expression for `ζ^3`, in IK between (1.30) and (1.31).
Proof
This is an alternative expression for \(\zeta(s)^3\) that can be derived from the previous results. By expressing \(\zeta(s)^3\) in terms of the L-series of \(\tau(n^2)\) and using the properties of Dirichlet convolutions, we can rewrite the sum in a way that involves summing over divisors \(d\) and corresponding \(m\) such that \(d^2 m = n\). This rearrangement of the series allows us to express \(\zeta(s)^3\) in the desired form.
Lean
Stated as ArithmeticFunction.zeta_pow_three_eq_alt; the blueprint marks no proof of it as formalized.
Sources
Theoremtwo-pow-omega-le-sigma-zero#
We have the inequality \(2^{\omega(n)}\leq\sigma_0(n)\) when \(n\neq 0\).
Proof
Recall that \(\omega(n)\) is the number of distinct prime factors of \(n\). Thus,
Likewise, \(\sigma_0(n)\) is the number of divisors of \(n\). We can write this as
where \(v_p(n)\) denotes the \(p\)-adic valuation of \(n\). For \(p|n\) we have that \(2\leq 1+v_p(n)\). Thus the result immediately follows.
Lean
Formalized as ArithmeticFunction.two_pow_omega_le_sigma_zero.
Sources
Used by 1
TheoremLSeriesSummable-two-pow-omega#
An L-series is convergent if the absolute value of each term is term wise less than a summable series.
Proof
Apply triangle inequality and comparison test.
Lean
Formalized as ArithmeticFunction.LSeriesSummable.of_norm_le_norm, ArithmeticFunction.LSeriesSummable_two_pow_omega.
Sources
Uses 4 · Used by 5
TheoremLSeries.term-isMultiplicative-if-fun-isMultiplicative#
If \(f\) is a multiplicative function, then so to is \(n\mapsto f(n)/n^s\).
Proof
Note that \(f(mn)/(mn)^s=f(m)f(n)/(m^sn^s)=(f(m)/m^s)(f(n)/n^s)\).
Lean
Formalized as ArithmeticFunction.LSeries.term_isMultiplicative_if_fun_isMultiplicative.
Sources
TheorempowOfAdditive-isMultiplicative#
If \(f\) is an additive function, then so to is \(n\mapsto k^{f(n)}\) for any fixed \(k\).
Proof
Note that \(k^{f(mn)}=k^{f(m)+f(n)}=k^{f(m)}k^{f(n)}\).
Lean
Formalized as ArithmeticFunction.powOfAdditive_isMultiplicative.
Sources
Uses 1 · Used by 1
Theoremtwo-pow-omega-isMultiplicative#
The function \(n\mapsto 2^{\omega(n)}\) is multiplicative.
Proof
This follows directly from Lemma powOfAdditive-isMultiplicative and the fact that \(\omega(mn)=\omega(m)+\omega(n)\).
Lean
Formalized as ArithmeticFunction.two_pow_omega_isMultiplicative.
Sources
Uses 1 · Used by 1
Theoremtwo-pow-omega-LSeries.term-isMultiplicative#
We have that \(n\mapsto 2^{\omega(n)}/n^{s}\) is a multiplicative function.
Proof
Follows as a consequence of Lemma LSeries.term-isMultiplicative-if-fun-isMultiplicative and two-pow-omega-isMultiplicative.
Lean
Formalized as ArithmeticFunction.two_pow_omega_LSeries.term_isMultiplicative.
Sources
Uses 2 · Used by 2
DefinitionsumOnPrimePows#
Shorthand for the sum of a function \(f:\mathbb{N}\to\mathbb{C}\) at prime powers for a prime \(p\).
TheoremsumOnPrimePows-apply#
Helper lemma for sumOnPrimePows that rewrites the shorthand as its sum.
Uses 1 · Used by 5
Theoremtwo-pow-omega-tsum-prime-pow#
For \(1\lt \Re(s)\) and \(p\) prime, we have that
Proof
Note that \(\omega(p^0)=0\) and \(\omega(p^k)=1\) whenever \(0\lt k\). Thus,
Now apply a geometric sum to the non-constant terms and simplify. We have the necessary convergence as \(1\lt \Re(s)\).
Lean
Formalized as ArithmeticFunction.two_pow_omega_tsum_prime_pow.
Sources
Uses 3 · Used by 2
TheoremComplex.one-add-prime-cpow-ne-zero#
For \(1\lt \Re(s)\) and \(p\) prime, we have that \(1+p^{-s}\neq 0\). The naming convention is to mimic
Complex.one_sub_prime_cpow_ne_zero
Proof
Suppose for contradiction \(1+p^{-s}=0\), then \(|p^{-s}|=1\). However, this can not happen per
Complex.norm_prime_cpow_le_one_half
Lean
Formalized as ArithmeticFunction.Complex.one_add_prime_cpow_ne_zero.
Sources
Used by 3
Theoremtwo-pow-omega-LSeries-eulerProduct-tprod#
For \(1\lt \Re(s)\) we have that
The naming convention here is designed to match
riemannZeta_eulerProduct_tprod
Proof
Immediately follows from Lemmas two-pow-omega-LSeries.term-IsMultiplicative and two-pow-omega-tsum-prime-pow.
Lean
Formalized as ArithmeticFunction.two_pow_omega_LSeries_eulerProduct_tprod.
Sources
Uses 5 · Used by 1
Theoremtwo-pow-omega-LSeries-eulerProduct-hasProd#
For \(1\lt \Re(s)\) we have that
The naming convention here is designed to match
riemannZeta_eulerProduct_hasProd
Proof
Immediately follows from Lemmas two-pow-omega-LSeries.term-IsMultiplicative and two-pow-omega-tsum-prime-pow.
Lean
Formalized as ArithmeticFunction.two_pow_omega_LSeries_eulerProduct_hasProd.
Sources
Uses 3 · Used by 1
Theoremzeta pow two#
for \(\Re(s) > 1\).
An expression for `ζ^2`, in IK (1.31).
Proof
Note that
Similarly
Applying Theorems two-pow-omega-LSeries-eulerProduct-tprod and two-pow-omega-LSeries-eulerProduct-hasProd we have
Thus
by the difference of squares. This is exactly the Euler product for \(\zeta(s)^2\) mentioned earlier.
Lean
Formalized as ArithmeticFunction.zeta_pow_two.
Sources
Theoremzeta pow three eq#
Zeta cubed: \(\zeta(s)^3 = \zeta(2s) \sum_{n=1}^{\infty}\tau(n^2) n^{-s}\) for \(\Re(s) > 1\).
This is IK (1.30).
Proof
Direct Euler-product proof (independent of Ramanujan / Baby Rankin–Selberg). Locally \(\tau((p^k)^2)=\tau(p^{2k})=2k+1\), and \(\sum_k(2k+1)x^k=(1+x)/(1-x)^2\) for \(|x|<1\). Multiplying by the local factor \(1/(1-x^2)\) of \(\zeta(2s)\) recovers \(1/(1-x)^3\), the local factor of \(\zeta(s)^3\). Absolute convergence follows by comparing \(\tau(n^2)\le d_3(n)\).
Lean
Formalized as ArithmeticFunction.zeta_pow_three_eq.
Sources
TheoremLSeriesSummable-moebius-sq#
The \(L\)-series with coefficients given by \(\mu^2(n)\) converges on the region \(1\lt \Re(s)\).
Proof
This follows by comparison test against the Riemann zeta function.
Lean
Formalized as ArithmeticFunction.LSeriesSummable_moebius_sq.
Sources
Uses 1 · Used by 2
TheorempowOfMultiplicative-isMultiplicative#
If \(f\) is a multiplicative function, then so to is \(n\mapsto f(n)^k\) for any \(k\in\mathbb{N}\).
Proof
Note that \(f(mn)^k=(f(m)f(n))^k=(f(m)^k)(f(n)^k)\).
Lean
Formalized as ArithmeticFunction.powOfMultiplicative_isMultiplicative.
Sources
Used by 1
Theoremmoebius-sq-LSeries.term-isMultiplicative#
We have that \(n\mapsto \mu^2(n)/n^{s}\) is a multiplicative function.
Proof
Follows as a consequence of Lemma LSeries.term-isMultiplicative-if-fun-isMultiplicative and moebius-sq-isMultiplicative.
Lean
Formalized as ArithmeticFunction.moebius_sq_LSeries.term_isMultiplicative.
Sources
Uses 2 · Used by 2
Theoremmoebius-sq-tsum-prime-pow#
For \(p\) prime, we have that
Proof
Note that \(\mu^2(p^0)=1\) and \(\mu^2(p^1)=1\) but \(\mu^2(p^k)=0\) whenever \(1\lt k\). Thus,
Lean
Formalized as ArithmeticFunction.moebius_sq_tsum_prime_pow.
Sources
Uses 2 · Used by 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.