sigmaR-apply to zeta mul tau square eq
TheoremsigmaR-apply#
We have that \(\sigma^R_s(n)=\sum_{d\mid n}d^s.\)
Proof
This follows immediately from the definition.
Lean
Formalized as ArithmeticFunction.sigmaR_apply.
Sources
Uses 1 · Used by 7
TheoremsigmaR-natCast'#
A casting lemma for \(\sigma^R\).
Uses 3
TheoremsigmaR-apply-prime-pow#
For a prime power, we have that \(\sigma^R_s(p^i)=\sum_{j=0}^ip^{js}\).
Proof
Note that \(d\mid p^i\) implies that \(d=p^j\) with \(0\leq j\leq i\). Thus,
Lean
Formalized as ArithmeticFunction.sigmaR_apply_prime_pow.
Sources
Uses 2 · Used by 3
TheoremsigmaR-one-apply#
Same as the previous lemma, but with a different casting structure.
Uses 2
TheoremsigmaR-one-apply-prime-pow#
Same as the previous lemma, but with a different casting structure.
Uses 2
TheoremsigmaR-eq-sum-div#
We have that \(\sigma^R_s(n)=\sum_{d\mid n}(n/d)^s\).
Proof
Note that \(d \mapsto n/d\) forms a one-to-one mapping between the divisors of \(n\). Using this in combination with the definiton we have that
Lean
Formalized as ArithmeticFunction.sigmaR_eq_sum_div.
Sources
Uses 2
TheoremsigmaR-zero-apply#
Same as the previous lemma, but with a different casting structure.
Uses 2
TheoremsigmaR-zero-apply-prime-pow#
Same as the previous lemma, but with a different casting structure.
Uses 2
TheoremsigmaR-one#
We have that \(\sigma^R_s(1)=1\).
Proof
By definition we have that
Lean
Formalized as ArithmeticFunction.sigmaR_one.
Sources
Uses 2
DefinitionpowR#
Arithmetic function with complex parameter \(\nu\). Evaluates as \(n\mapsto n^{\nu}\) for \(n\neq 0\) and \(0\) at \(n=0\).
TheoremisMultiplicative-powR#
For fixed \(\nu\) the function \(n\mapsto n^\nu\) is multiplicative.
Proof
This immediately follows from the fact that exponentiation with a fixed power is a homomorphism.
Lean
Formalized as ArithmeticFunction.isMultiplicative_powR.
Sources
Uses 1 · Used by 1
TheoremsigmaR-eq-zeta-mul-powR#
\(\sigma^R(\nu) = \zeta * \text{pow}^R(\nu)\), where \(\zeta\) is the constant function \(1\).
Proof
The function \(\sigma^R(\nu)\) is defined as the sum of the \(\nu\)-th powers of the divisors of \(n\). The function \(\text{pow}^R(\nu)\) is defined as \(n \mapsto n^\nu\) for \(n \neq 0\) and \(0\) for \(n = 0\). The Dirichlet convolution of \(\zeta\) (the constant function \(1\)) and \(\text{pow}^R(\nu)\) is exactly \(\sigma^R(\nu)\), since for each divisor \(d\) of \(n\), we have \((\zeta * \text{pow}^R(\nu))(n) = \sum_{d|n} 1 \cdot d^\nu = \sigma^R(\nu)(n)\). Thus, we have \(\sigma^R(\nu) = \zeta * \text{pow}^R(\nu)\).
Lean
Formalized as ArithmeticFunction.sigmaR_eq_zeta_mul_powR.
Sources
Uses 3 · Used by 2
TheoremisMultiplicative-sigmaR#
For fixed \(s\) function \(n\mapsto\sigma^R_s(n)\) is multiplicative.
Proof
Recall from Lemma sigmaR-eq-zeta-mul-powR that \(\sigma^R\) is \(\zeta\) convolved with Definition powR. Since both of these are multiplicative functions, their convolution is also multiplicative.
Lean
Formalized as ArithmeticFunction.isMultiplicative_sigmaR.
Sources
Uses 4 · Used by 1
TheoremsigmaR-eq-prod-primeFactors-sum-range-factorization-pow-mul#
We have that
Proof
Since \(\sigma^R_s\) is multiplicative, it suffices to understand it at primes powers.
Applying Lemma sigmaR-apply-prime-pow.
Lean
Formalized as ArithmeticFunction.sigmaR_eq_prod_primeFactors_sum_range_factorization_pow_mul.
Sources
Uses 3
TheoremLSeries powR eq#
\(L(\text{pow}^R(\nu), s) = \zeta(s - \nu)\) for \(\Re(s - \nu) > 1\).
This is IK (1.27).
Proof
The function \(\text{pow}^R(\nu)\) is defined as \(n \mapsto n^\nu\) for \(n \neq 0\) and \(0\) for \(n = 0\). The L-series of \(\text{pow}^R(\nu)\) at \(s\) is given by the sum \(\sum_{n=1}^{\infty} n^{\nu - s}\). This series converges to the Riemann zeta function \(\zeta(s - \nu)\) for \(\Re(s - \nu) > 1\), since the zeta function is defined as \(\zeta(s) = \sum_{n=1}^{\infty} n^{-s}\) for \(\Re(s) > 1\). Therefore, we have \(L(\text{pow}^R(\nu), s) = \zeta(s - \nu)\) under the condition that \(\Re(s - \nu) > 1\).
Lean
Formalized as ArithmeticFunction.LSeries_powR_eq.
Sources
Uses 1 · Used by 2
Theoremabscissa powR le#
The abscissa of absolute convergence of \(L(\text{pow}^R(\nu), s)\) is at most \(\Re(\nu) + 1\).
Proof
We apply LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow which states that if there exists a constant \(C\) such that \(\|f(n)\| \leq C \cdot n^r\) for all \(n\) sufficiently large, then the abscissa of absolute convergence of \(L(f, s)\) is at most \(r + 1\). In our case, we can take \(f(n) = n^\nu\) and observe that \(\|n^\nu\| = n^{\Re(\nu)}\). Thus, we can choose \(C = 1\) and \(r = \Re(\nu)\), which gives us the desired result that the abscissa of absolute convergence of \(L(\text{pow}^R(\nu), s)\) is at most \(\Re(\nu) + 1\).
Lean
Formalized as ArithmeticFunction.abscissa_powR_le.
Sources
Uses 1 · Used by 1
TheoremLSeries sigma eq riemannZeta mul#
\(\zeta(s)\zeta(s - \nu) = \sum_{n=1}^{\infty} \sigma_\nu(n) n^{-s}\) for \(\Re(s) > 1\) and \(\Re(s - \nu) > 1\).
Proof
The divisor power sum function \(\sigma_\nu\) is the Dirichlet convolution of the constant function \(1\) (i.e., \(\zeta\)) and the power function \(n \mapsto n^\nu\). The L-series of a Dirichlet convolution is the product of the L-series of the individual functions. Since \(L(1, s) = \zeta(s)\) and \(L(n \mapsto n^\nu, s) = \zeta(s - \nu)\), we have \(L(\sigma_\nu, s) = \zeta(s) \cdot \zeta(s - \nu)\) for \(\Re(s) > 1\) and \(\Re(s - \nu) > 1\).
Lean
Formalized as ArithmeticFunction.LSeries_sigma_eq_riemannZeta_mul.
Sources
Uses 5
Theoremzeta mul zeta mul zeta mul zeta eq#
Ramanujan formula: \(\zeta(s)\zeta(s-\alpha)\zeta(s-\beta)\zeta(s-\alpha-\beta)=\zeta(2s-\alpha-\beta) \sum_{n=1}^{\infty} \sigma_\alpha(n)\sigma_\beta(n)n^{-s}\) for \(\Re(s) > 1\), \(\Re(s-\alpha) > 1\), \(\Re(s-\beta) > 1\), and \(\Re(s-\alpha-\beta) > 1\).
This is IK (1.28).
Proof
This is a direct consequence of the multiplicative properties of the functions involved and the definition of the L-series. The left-hand side can be expressed as a product of L-series corresponding to the functions \(\zeta\), \(n \mapsto n^{-\alpha}\), and \(n \mapsto n^{-\beta}\). The right-hand side involves the L-series of the convolution of \(\sigma_\alpha\) and \(\sigma_\beta\), which can be expressed in terms of the L-series of \(\zeta\) and the power functions. By carefully applying the properties of Dirichlet convolutions and the definitions of the L-series, we can derive the stated formula.
Lean
Stated as ArithmeticFunction.zeta_mul_zeta_mul_zeta_mul_zeta_eq; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
Theoremzeta pow four eq#
Corollary: \(\zeta(s)^4 = \zeta(2s) \sum_{n=1}^{\infty} \tau(n)^2 n^{-s}\) for \(\Re(s) > 1\).
This is IK (1.29).
Proof
This is a special case of the previous theorem where we set \(\alpha = \beta = 0\).
Lean
Formalized as ArithmeticFunction.zeta_pow_four_eq.
Sources
Uses 2 · Used by 1
Theoremzeta mul tau square eq#
Baby Rankin-Selberg: \(\zeta(s)\sum_{n=1}^{\infty}\tau(n^2)n^{-s} = \sum_{n=1}^{\infty}\tau(n)^2 n^{-s}\) for \(\Re(s) > 1\).
Precursor to IK (1.30).
Proof
This follows from the multiplicative properties of the divisor function \(\tau\) and the definition of the L-series. The left-hand side can be expressed as a product of L-series corresponding to \(\zeta\) and the function \(n \mapsto \tau(n^2)\). The right-hand side is the L-series of the function \(n \mapsto \tau(n)^2\). By analyzing the Euler products and using the fact that \(\tau(n)\) counts divisors, we can derive the stated equality.
Lean
Formalized as ArithmeticFunction.zeta_mul_tau_square_eq.
Sources
Uses 5 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.