Part of: The mod-4 character, the k = 2 and k ≥ 3 layers of the Euler-product logarithm, the power series of the logarithm, and the divergence transfer.
DefinitionlayerT
The k \ge 3 layer T(s) = \sum_p t_p(s), summed over all primes. The per-prime bound
|t_p| \le \tfrac43 p^{-3/2} feeds the Weierstrass M-test, so T is holomorphic on
\Omega with the uniform bound \|T(s)\| \le c_T := \tfrac43 \sum_p p^{-3/2} on
\mathrm{Re}\, s \ge 1/2, and real on the real axis.
Lean code for Definition layerT
-
⟲
def layerT (s
ℂ: ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.def layerT (s
ℂ: ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.
⟲:= ∑' pNat.Primes : Nat.PrimesNat.Primes : TypeThe type of prime numbers , tpA362583.tp (p : Nat.Primes) (s : ℂ) : ℂPer-prime `k ≥ 3` tail `t_p(s) = Σ_{k≥0} (χ(p) p^(-s))^(k+3) / (k+3)`.
The compact form `z_p^(k+3)/(k+3)` (rather than the expanded
`χ(p)^(k+3) p^(-(k+3)s)/(k+3)`) is chosen so that the tail produced by peeling three
terms off `hasSum_neg_log_one_sub` is *definitionally* `tp p s` (see `neg_log_split`). pNat.Primes sℂ