Part of: The k = 1 layer, the split of the Euler-product logarithm into layers, the identity exp(A + B + T) = L(s, χ), and the coefficient bridge to the race sum.
DefinitionlayerA
The k = 1 layer. A(s) = \sum_p \chi(p)\, p^{-s}, absolutely convergent for
\mathrm{Re}\, s > 1. This is the layer that carries the race: everything the analytic
argument ever learns about the distribution of the bits flows through A.
Lean code for Definition layerA
-
⟲
def layerA (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 layerA (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 , χA362583.χ : DirichletCharacter ℂ 4The project Dirichlet character mod 4, `ZMod.χ₄` pushed to `ℂ`. ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.
This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`. 4ℕ) * ((pNat.Primes : ℕNat : TypeThe natural numbers, starting at zero.
This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. ) ^ (-sℂ)